In this section:
Wed, 08 Aug 2018
In my original article, I said:
Jeremy Yallop brought up an example that I had definitely seen before.
In 2008 Conor McBride and Ross Paterson wrote an influential paper, “Idioms: applicative programming with effects” that introduced the idea of an applicative functor, a sort of intermediate point between functors and monads. It has since made its way into standard Haskell and was deemed sufficiently important to be worth breaking backward compatibility.
McBride and Paterson used several notations for operations in an
applicative functor. Their primary notation was !!\iota!! for what is
now known as
$$\iota f \circledast is_1 \circledast \ldots \circledast is_n$$
came up so often they wanted a less cluttered notation for it:
On page 5, they suggested an exercise:
They give a hint, intended to lead the reader to the solution, which
involves a function named
and have it mean
The haskell wiki has details, written by Don Stewart when the McBride-Paterson paper was still in preprint. The wiki goes somewhat further, also defining
now does a
I have certainly read this paper more than once, and I was groping for this example while I was writing the original article, but I couldn't quite put my finger on it. Thank you, M. Yallop!
[ By the way, I am a little bit disappointed that the haskell wiki is not called “Hicki”. ]
In the previous article I described a rather odd abuse of the Haskell type system to use a singleton type as a sort of pseudo-keyword, and asked if anyone had seen this done elsewhere.
so that they can end every proof with
This example is from Vazou et al., Functional Pearl: Theorem Proving
for All, p. 3. The authors
Or see the examples from the bottom of the LH splash
page, proving the
associative law for
I looked in the rest of the LiquidHaskell distribution but did not find any other uses of the singleton-type trick. I would still be interested to see more examples.
[ Addendum: Another example. ]
A friend asked me the other day about techniques in Haskell to pretend
to make up keywords. For example, suppose we want something like a
This uses a condition
Now suppose for whatever reason we don't like writing it as
Now we can write
But then I had a surprising idea. We can define it this way:
Now we write
and if we omit or misspell the
For a less trivial (but perhaps sillier) example, consider:
The idea here is that we want to try a computation, and do one thing
if it succeeds and another if it throws an exception. The point is
not the usefulness of this particular and somewhat contrived exception
handling construct, it's the syntactic sugar of the
I was fairly confident I had seen something like this somewhere before, and that it was not original to me. But I've asked several Haskell experts and nobody has said it was familar. I thought perhaps I had seen it somewhere in Brent Yorgey's code, but he vehemently denied it.
So my question is, did I make up this technique of using a one-element type as a pretend keyword?
[ Addendum: At least one example of this trick appears in LiquidHaskell. I would be interested to hear about other places it has been used. ]
[ Addendum: Jeremy Yallop points out that a similar trick was hinted at in McBride and Paterson “Idioms: applicative programming with effects” (2008), with which I am familiar, although their trick is both more useful and more complex. So this might have been what I was thinking of. ]