Output for (a -> Bool) -> [a] -> [a]:
forall t1,t2 in TYPES, R in REL(t1,t2).
forall p :: t1 -> Bool.
forall q :: t2 -> Bool.
(forall (x, y) in R. p x = q y)
==> (forall (z, v) in lift{[]}(R).
(f_{t1} p z, f_{t2} q v) in lift{[]}(R))
lift{[]}(R)
= {([], [])}
u {(x : xs, y : ys) | ((x, y) in R) && ((xs, ys) in lift{[]}(R))}forall t1,t2 in TYPES, g :: t1 -> t2.
forall p :: t1 -> Bool.
forall q :: t2 -> Bool.
(forall x :: t1. p x = q (g x))
==> (forall y :: [t1].
map_{t1}_{t2} g (f_{t1} p y) = f_{t2} q (map_{t1}_{t2} g y))TIL:
In the context of GHC, zonking is when a type is traversed and mutable type variables are replaced with the real types they dereference to.
Most interesting example:
_ [3,1,2] :: Sorted (O(N*.LogN)) (O(N)) Integer
Valid hole fits include
mergeSort :: forall (n :: AsymP) (m :: AsymP) a.
(n >=. O (N *. LogN), m >=. O N, Ord a)
=> [a] -> Sorted n m a
quickSort :: forall (n :: AsymP) (m :: AsymP) a.
(n >=. O (N *. LogN), m >=. O LogN, Ord a)
=> [a] -> Sorted n m aJules Hedges on connections between lenses, the dialectica interpretation, backprop, etc.
List of “top algorithms”. Take with a huge grain of salt. Interesting list to look through though.
There is a data structure called a discrimination tree that allows one to compactly store a large number of terms (rose trees) with metavariables and then, given another term with metavariables, efficiently filter the set of contained terms down to a subset that may unify with the given term.
Best discussion I’ve seen of the practicalities of running a prediction market.
The weakness (or twist) on markets this implies applies to prediction markets generally. If you bet on an event that is correlated with the currency you’re betting in, the fair price can be very different from the true probability. It doesn’t have to be price based – think about betting on an election between a hard money candidate and one who will print money, or a prediction on a nuclear war.
If I bet on a nuclear war, and win, how exactly am I getting paid?
Also,
There are three types of prediction markets that have gotten non-zero traction.
To get a thriving market, you need (at least) these five things
Do read the whole thing.
Interesting question and interesting answer by Neel K. I’ve been seeing Bekic’s lemma everywhere lately.
Handling of effects in the denotational framework, however, proved to be much more problematic, often summed up by the phrase “denotational semantics is not modular”. Briefly, addition of new effects require substantial changes to the existing semantic description. For instance, exceptions can be modeled by adding a special failure element to each domain, representing the result of a failed computation. But then, even such a simple thing as the meaning of an arithmetic operation requires a messy denotational description; one needs to check for failure at each argument, and propagate accordingly. The story is similar for other cases, including I/O and assignments, two of the most “popular” effects found in many programming languages.
It was Moggi’s influential work on monads that revolutionized the semantic treatment of effects, which he referred to as notions of computation. Moggi showed how monads can be used to model programming language features in a uniform way, providing an abstract view of programming languages. In the monadic framework, values of a given type are distinguished from computations that yield values of that type. Since the monadic structure hides the details of how computations are internally represented and composed, programmers and language designers work in a much more flexible environment. This flexibility is a huge win over the traditional approach, where everything has to be explicit.
Perhaps what Moggi did not quite envision was the response from the functional programming community, who took the idea to heart. Wadler wrote a series of articles showing how monads can be used in structuring functional programs themselves, not just the underlying semantics. Very quickly, the Haskell committee adopted monadic I/0 as the standard means of performing input and output in Haskell, making monads an integral part of a modern programming language. The use of monads in Haskell is further encouraged by special syntactic support, known as the do-notation.
As the monadic programming style became more and more popular in Haskell, programmers started realizing certain shortcomings. For instance, function application becomes tedious in the presence of effects. Or, the if-then-else construct becomes unsightly when the test expression is monadic. However, these are mainly syntactic issues that can easily be worked around. More seriously, the monadic sublanguage lacks support for recursion over the values of monadic actions. The issue is not merely syntactic; it is simply not clear what a recursive definition means when the defining expression can perform monadic effects.
This problem brings us to the subject matter of the present work: Semantics of recursive declarations in monadic computations. More specifically, our aim is to study recursion resulting from the cyclic use of values in monadic actions. We use the term value recursion to describe this notion.