Generic support for programming with names and binders https://github.com/sweirich/replib

Version on this page:0.5.1
LTS Haskell 8.3:0.5.1
Stackage Nightly 2017-02-26:0.5.1
Latest on Hackage:0.5.1
-- Copyright : (c) 2010-2015, Unbound team (see LICENSE)
-- License : BSD3
-- Maintainer : sweirich@cis.upenn.edu, byorgey@cis.upenn.edu
-- Stability : experimental
-- Portability : non-portable

Specify the binding structure of your data type with an expressive set
of type combinators, and Unbound handles the rest! Automatically
derives alpha-equivalence, free variable calculation, capture-avoiding
substitution, and more.

To install:

cabal install unbound

To get started using the library, see the tutorial in the tutorial/
directory and the extensive Haddock documentation (start with the
Unbound.LocallyNameless module).


Version 0.2: 24 March 2011

* Initial release to go along with submission of "Binders Unbound".

Version 0.2.1: 28 March 2011

* Massive update to documentation.

Version 0.2.2: 29 March 2011

* Add MonadFix instances for FreshM and LFreshM. Thanks to Job
Vranish for the suggestion.

Version 0.2.3: 20 April 2011

* Fix minor bugs in
- tutorial/Tutorial.lhs
- examples/Abstract.hs
- examples/STLC.hs

Thanks to Ki Yung Ahn for the reports.

Version 0.2.5: 13 July 2011

* Fix bug in mkPerm which caused unbind2 to unexpectedly fail when
dealing with binders with non-disjoint sets of names.

Thanks to Sean Leather for the report.

* Clean up some compiler warnings.

Version 0.3: 24 August 2011

* New permutation- and set-binding functions, for creating binders
which don't care about the order of multiple bound names, and/or
about unused bound names.

* Bump RepLib dependency to 0.5, which now has support for GADTs
without existential type variables.

Version 0.3.1: 25 August 2011

* Update to build on GHC 7.2.1

Version 0.4: 15 March 2012

* Update to build on GHC 7.4.1

* add MonadWriter instances for FreshMT and LFreshMT

* Make 'getAvoids' function into a method of the LFresh class

Version 23 March 2012

* Remove broken links from documentation

Version 10 April 2012

* Bump 'mtl' upper bound to allow mtl-2.1

Version 0.4.1: 5 June 2012

* Patch from Vilhelm Sjöberg changing acompareR1 to return EQ for

Version 21 Aug 2012

* Bump containers upper bound and test with GHC 7.6.1

Version 0.4.2: 15 July 2013

* remove derived instances: MonadState for FreshMT and MonadReader
for LFreshMT. No one should have been using these anyway, and
they made it impossible to use these transformers together with
your own state.

* added unbind variants [l]unbind{23}Plus for conveniently unbinding
in a MonadPlus context.

Version 0.4.3: 29 January 2014

* Add Binary instances for Name, GenBind, Rebind, and Embed.

Note that although the PVP requires a major version bump for added
instances, it was impossible to write these instances outside of
the package, so there is no danger of breakage.

Version 8 May 2014

* Allow transformers-0.4 and mtl-2.2

Version 0.4.4: 18 May 2015

* Update to work with GHC 7.10

Version 0.4.5: 2 Oct 2015

* Test suite in cabal file
* New optimized function for immediately substitution w/o naming
Only works for patterns with a single variable:
substBind :: Subst a b => Bind (Name a) b -> a -> b

Version 0.5: August 2016

* Remove Show superclass for Alpha (potentially breaking change)
* Remove permValid function from Unbound.PermM

* New function in Unbound.LocallyNameless.Ops
patUnbind :: (Alpha p, Alpha t) => p -> Bind p t -> t
* More sensible Show instance for bind, shows as code that
can be directly parsed to Haskell.
old: <a> (Var 0@0)
new: (bind (string2Name "a") (Var (string2Name "a"))
* works with GHC-8.0.1
* Error message if don't override aeq' / acompare' for abstract types
* More correctness tests

Version 0.5.1: August 2016
* Fix testsuite compilation problem

Planned extensions:
* Cache free variables at binders
Used by 2 packages:
comments powered byDisqus