The Universe of Disco

A fake keyword example

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.

Joachim Breitner reported having seen this before. Most recently in LiquidHaskell, which defines a QED singleton type:

 data QED = QED
 infixl 2 ***

 (***) :: a -> QED -> Proof
 _ *** _ = ()

so that they can end every proof with *** QED:

singletonP x
      =   reverse [x]
      ==. reverse [] ++ [x]
      ==. [] ++ [x]
      ==. [x]
      *** QED

This example is from Vazou et al., Functional Pearl: Theorem Proving for All, p. 3. The authors explain: “The QED argument serves a purely aesthetic purpose, allowing us to conclude proofs with *** QED.”.

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. ]

[Other articles in category /prog/haskell] permanent link