# The Universe of Discourse

Wed, 08 Aug 2018

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.