unboundgenerics
Support for programming with names and binders using GHC Generics http://github.com/lambdageek/unboundgenerics
Version on this page:  0.4.0 
LTS Haskell 13.7:  0.4.0 
Stackage Nightly 20190217:  0.4.0 
Latest on Hackage:  0.4.0 
Module documentation for 0.4.0
 Unbound
 Unbound.Generics
 Unbound.Generics.LocallyNameless
 Unbound.Generics.LocallyNameless.Alpha
 Unbound.Generics.LocallyNameless.Bind
 Unbound.Generics.LocallyNameless.Embed
 Unbound.Generics.LocallyNameless.Fresh
 Unbound.Generics.LocallyNameless.Ignore
 Unbound.Generics.LocallyNameless.Internal
 Unbound.Generics.LocallyNameless.LFresh
 Unbound.Generics.LocallyNameless.Name
 Unbound.Generics.LocallyNameless.Operations
 Unbound.Generics.LocallyNameless.Rebind
 Unbound.Generics.LocallyNameless.Rec
 Unbound.Generics.LocallyNameless.Shift
 Unbound.Generics.LocallyNameless.Subst
 Unbound.Generics.LocallyNameless.TH
 Unbound.Generics.LocallyNameless.Unsafe
 Unbound.Generics.PermM
 Unbound.Generics.LocallyNameless
 Unbound.Generics
unboundgenerics
Support for programming with names and binders using GHC Generics.
Summary
Specify the binding structure of your data type with an expressive set of type combinators, and unboundgenerics
handles the rest! Automatically derives alphaequivalence, free variable calculation, captureavoiding substitution, and more. See Unbound.Generics.LocallyNameless
to get started.
This is a reimplementation of (parts of) unbound but using GHC generics instead of RepLib.
Examples
Some examples are in the examples/
directory in the source. And also at unboundgenerics on GitHub Pages
Example: Untyped lambda calculus interpreter
Here is how you would implement call by value evaluation for the untyped lambda calculus:
{# LANGUAGE DeriveDataTypeable, DeriveGeneric, MultiParamTypeClasses #}
module UntypedLambdaCalc where
import Unbound.Generics.LocallyNameless
import GHC.Generics (Generic)
import Data.Typeable (Typeable)
  Variables stand for expressions
type Var = Name Expr
  Expressions
data Expr = V Var  ^ variables
 Lam (Bind Var Expr)  ^ lambdas bind a variable within a body expression
 App Expr Expr  ^ application
deriving (Show, Generic, Typeable)
 Automatically construct alpha equivalence, free variable computation and binding operations.
instance Alpha Expr
 semiautomatically implement capture avoiding substitution of expressions for expressions
instance Subst Expr Expr where
 `isvar` identifies the variable case in your AST.
isvar (V x) = Just (SubstName x)
isvar _ = Nothing
 evaluation takes an expression and returns a value while using a source of fresh names
eval :: Expr > FreshM Expr
eval (V x) = fail $ "unbound variable " ++ show x
eval e@(Lam {}) = return e
eval (App e1 e2) = do
v1 < eval e1
v2 < eval e2
case v1 of
(Lam bnd) > do
 open the lambda by picking a fresh name for the bound variable x in body
(x, body) < unbind bnd
let body' = subst x v2 body
eval body'
_ > fail "application of nonlambda"
example :: Expr
example =
let x = s2n "x"
y = s2n "y"
e = Lam $ bind x (Lam $ bind y (App (V y) (V x)))
in runFreshM $ eval (App (App e e) e)
 >>> example
 Lam (<y> App (V 0@0) (Lam (<x> Lam (<y> App (V 0@0) (V 1@0)))))
Differences from unbound
For the most part, I tried to keep the same methods with the same signatures. However there are a few differences.

fv :: Alpha t => Fold t (Name n)
The
fv
method returns aFold
(in the sense of the lens library), rather than anUnbound.Util.Collection
instance. That means you will generally have to writetoListOf fv t
or some other summary operation. 
Utility methods in the
Alpha
class have different types.You should only notice this if you’re implementing an instance of
Alpha
by hand (rather than by using the default generic instance).isPat :: Alpha t => t > DisjointSet AnyName
The originalunbound
returned aMaybe [AnyName]
here with the same interpretation asDisjointSet
:Nothing
means an inconsistency was encountered, orJust
the free variables of the pattern.isTerm :: Alpha t => t > All
open :: Alpha t => AlphaCtx > NthPatFind > t > t
,close :: Alpha t => AlphaCtx > NamePatFind > t > t
whereNthPatFind
andNamePatFind
are newtypes

embed :: IsEmbed e => Embedded e > e
andunembed :: IsEmbed e => e > Embedded e
The typeclass
IsEmbed
has anIso
(again in the sense of thelens
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 implementembedded = iso yourEmbed yourUnembed
whereiso
comes fromlens
. (Although you can also implement it in terms ofdimap
if you don’t want to depend on lens)
Changes
NEXT
0.4.0

New binding specification type
Ignore
.Any two
Ignore T
terms will always be alphaequivalent to each other, will be considered to contain no variables, and will not have any substitution apply beneathIgnore
. Useful for attaching annotation terms to your AST.import Text.Parsec.Pos (SourcePos) data Expr = ...  Lambda (Ignore SourcePos) (Bind (Name Expr) Expr)
As expected, any two
Lambda
expressions will be considered alphaequivalent even if they differ in source position.Note that the
Ignore
will block operations onName a
for alla
, which can be a little unexpected:data Ty = TyVar (Name Ty)  TyArr Ty Ty instance Subst Ty Ty where ... data Expr = ...  Var (Name Expr)  Lambda (Ignore Ty) (Bind (Name Expr) Expr) instance Subst Ty Expr
Applying a substitution of a type for a free type variable to a
Lambda
will not descend into theIgnore Ty
.Thanks Reed Mullanix (TOTWBF) for the new operation.

Fix an issue in substitution where traversal would not continue in an AST node for which
isvar
orisCoerceVar
is defined to return nonNothing
but which had additional structure.For example, in a language with meta variables and explicit substitutions:
data Expr = ...  normal variables that stand for expressions  Var (Name Expr)  a meta variable occurrence and an explicit substitution  of expressions to substitute in for the free variables  MetaVar (Name Meta) [(Name Expr, Expr)]  a meta variable stands for an expression with some free term vars data Meta = MetaVar Expr  substitution for a meta in an expression instance Subst Expr Meta where isCoerceVar (MetaVar u sub) = Just (SubstCoerce u (Just . applyExplicitSubst sub)) applyExplicitSubst :: [(Name Expr, Expr)] > Meta > Expr applyExplicitSubst s (MetaVar e) = substs s e
Given an expression
e1
defined asMetaVar "u" [("x", 10)]
, we may want to substitute aMeta ("x" + "x")
for"u"
to get10 + 10
(that is, we replace"u"
by the expression"x" + "x"
and immediately apply the substitution10
for"x"
).Now suppose we have an expression
e2
defined asMetaVar "v" [("y", e1)]
(that is, an occurrence of meta var “v” together with a substitution ofe1
from above for"y"
). If we again try to substituteMeta ("x" + "x")
for"u"
ine2
, we would expect to getMetaVar "v" [("y", 10 + 10)]
(that is, since “v” is not equal to “u”, we leave the meta var alone, but substitute for any occurrences of “u” in the explicit substitution, soe1
becomes10 + 10
as before).The bug in previous versions of
unboundgenerics
was that we would incorrectly leaveMetaVar "v" [("y", e1)]
unchanged as soon as we saw thatisCoerceVar (MetaVar "v" [("y", e1)])
returnedJust (SubstCoerce "u" ...)
where"u" /= "v"
.Thanks Reed Mullanix (TOTWBF) for finding and fixing this issue. https://github.com/lambdageek/unboundgenerics/issues/26
0.3.4
 Bump
containers
upper bound to support0.6
. (GHC 8.6.1 support) Thanks Christiaan Baaij.
0.3.3
 Bump
exceptions
upper bound to support0.10.0
0.3.2
 Bump
deepseq >= 1.4.0.0
remove benchmark dependency ondeepseqgenerics
 Tested with GHC 8.4.1
 Tested with GHC 8.2.2
 Compile with
Wcompat
 Add
Semigroup
instances for all types that were previouslyMonoid
instances  Added more examples to the examples/ directory
 Added “exceptions” dependency and
MonadThrow
,MonadCatch
,MonadMask
instances forFreshMT
andLFreshMT
. Thanks Alex McKenna.
0.3.1
 Tested with GHC 8.0.1
 Removed
Generic b
constraint fromSubst b (Name a)
instance.
0.3
 Change types of
open
andclose
to takeNthPatFind
andNamePatFind
instead of generic patterns, update call sites.  Add newtype wrappers and Monoid instances for
NthPatFind
andNamePatFind
 Change
isTerm
to returnAll
instead ofBool
0.2

Incorporating some of the extras/oversights from clashlib Unbound.Generics.LocallyNameless.Extra
 Make
Embed
an instance ofOrd
NFData
instances (see below)
 Make

Reimplement
freshen'
andgfreshen
using a free monad to give GHC a chance to inline it all away. This changes the type ofgfreshen
. Major version bump. Expose
FFM
,liftFFM
andretractFFM
 Expose

Provide
NFData
instances for all the combinators. Depend on ‘deepseq’ 
Start benchmarking some of the operations (particularly
unbind
).
0.1.2.1
 Fix ghc7.10 build.
 Haddock cleanup.
0.1.2

Added
IsEmbed
typeclass Depend on ‘profunctors’

Changed
embed
andunembed
to work over anyIsEmbed
type. 
Added
Shift
type for shifting the scope of embedded terms out one level.
0.1.1
 Added
isNullDisjointSet
function.  Implement a TH
makeClosedAlpha
splice for constructing trivial leaf instances.
0.1

Add
acompare
functiona andacompare'
method toAlpha
typeclass. (christiaanb)Handwritten
Alpha
instances will need to define this additional method now. Major version bump.
0.0.3

Add ‘name2Integer’ method (christiaanb)

Export internal typedirected
gaeq
,gopen
,gclose
, etc functions fromUnbound.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)
0.0.2.1
 Unconditionally add ErrorT and ExceptT instances using transformerscompat (bergmark)
0.0.2

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

Alpha instance for ‘()’
0.0.1

Add ‘lunbind2’ function.

Doc updates.

Switch from ‘HUnit’ to ‘Tasty’ for testing.
0.0.0.90
 Initial (re)implementation effort.