Unbound now supports “set” binders and GADTs

I have just uploaded version 0.3 of the Unbound library (and version 0.5 of RepLib). This version adds support for two major new features:

• The new permbind and setbind functions create binders that are alpha-equivalent “up to permutation”. For example, when quantifying over a list of type variables, their order really does not matter: . Unbound now lets you express this and takes it into account when testing alpha-equivalence.
• RepLib (and hence Unbound) now supports GADTs, as long as they do not contain any existential quantification.

Enjoy!

Idempotent Template Haskell

Yesterday I was looking for a way to have some Template Haskell code generate a definition for a certain identifier if and only if such a definition did not already exist. Essentially I want to be able to call the code multiple times but have it generate something only once. This turns out to be extremely easy but non-obvious, so I thought I’d write it here for posterity. The trick is that reify throws an error if called on an identifier that doesn’t exist, and recover can be used to catch TH errors. Thus:

recover (generateBinding n) (reify n >> return [])

which uses generateBinding n to “recover” from the error of n‘s non-existence.