Unbound now supports “set” binders and GADTs

Posted on August 24, 2011 by Brent

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.

Enjoy!

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

Enter your comment here...

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

Email (required) (Address never made public)

Name (required)

Website

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

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

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

Connecting to %s