Build Status

This is a reimplementation of (parts of) unbound but using GHC generics instead of RepLib.

Differences from unbound

For the most part, I tried to keep the same methods with the same signatures. However there are a few differences.

  1. fv :: Alpha t => Fold t (Name n)

    The fv method returns a Fold (in the sense of the lens library), rather than an Unbound.Util.Collection instance. That means you will generally have to write toListOf fv t or some other summary operation.

  2. isPat :: Alpha t => t -> DisjointSet AnyName

    You should only notice this if you’re implementing an instance of Alpha by hand (rather than by using the default generic instance). The original unbound returned a Maybe [AnyName] here with the same interpretation as DisjointSet: Nothing means an inconsistency was encountered, or Just the free variables of the pattern.

  3. embed :: IsEmbed e => Embedded e -> e and unembed :: IsEmbed e => e -> Embedded e

    The typeclass IsEmbed has an Iso (again in the sense of the lens library) as a method instead of the above pair of methods.

    Again, you should only notice this if you’re implementing your own types that are instances of IsEmbed. The easiest thing to do is to use implement embedded = iso yourEmbed yourUnembed where iso comes from lens. (Although you can also implement it in terms of dimap if you don’t want to depend on lens)


  • Fix ghc-7.10 build.
  • Haddock cleanup.


  • Added IsEmbed typeclass

    • Depend on ‘profunctors’
  • Changed embed and unembed to work over any IsEmbed type.

  • Added Shift type for shifting the scope of embedded terms out one level.


  • Added isNullDisjointSet function.
  • Implement a TH makeClosedAlpha splice for constructing trivial leaf instances.


  • Add acompare functiona and acompare' method to Alpha typeclass. (christiaanb)

    Handwritten Alpha instances will need to define this additional method now. Major version bump.


  • Add ‘name2Integer’ method (christiaanb)

  • Export internal type-directed gaeq, gopen, gclose, etc functions from Unbound.Generics.LocallyNameless.Alpha.

    Allows definitions like:

      instance Alpha Term where
        aeq' _ (Prim t1 _dk1) (Prim t2 _dk2) = t1 == t2
        aeq' c t1             t2             = gaeq c (from t1) (from t2)

  • Unconditionally add ErrorT and ExceptT instances using transformers-compat (bergmark)


  • Add ‘Rec’ pattern and ‘TRec’ term combinators.

  • Alpha instance for ‘()’


  • Add ‘lunbind2’ function.

  • Doc updates.

  • Switch from ‘HUnit’ to ‘Tasty’ for testing.

  • Initial (re-)implementation effort.