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: \forall a b. a \to b \approx \forall b a. a \to b. 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.


This entry was posted in haskell, projects. Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s