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