bound
Making de Bruijn Succ Less http://github.com/ekmett/bound/
LTS Haskell 6.35:  1.0.7 
Stackage Nightly 20170721:  2 
Latest on Hackage:  2 
Module documentation for 1.0.7
Bound
Goals
This library provides convenient combinators for working with "locallynameless" terms. These can be useful when writing a type checker, evaluator, parser, or pretty printer for terms that contain binders like forall or lambda, as they ease the task of avoiding variable capture and testing for alphaequivalence.
See the documentation on hackage for more information, but here is an example:
{# LANGUAGE DeriveFunctor #}
{# LANGUAGE DeriveFoldable #}
{# LANGUAGE DeriveTraversable #}
{# LANGUAGE TemplateHaskell #}
import Bound
import Control.Applicative
import Control.Monad
import Data.Functor.Classes
import Data.Foldable
import Data.Traversable
import Data.Eq.Deriving (deriveEq1)  these two are from the
import Text.Show.Deriving (deriveShow1)  derivingcompat package
infixl 9 :@
data Exp a = V a  Exp a :@ Exp a  Lam (Scope () Exp a)
deriving (Eq,Show,Functor,Foldable,Traversable)
instance Applicative Exp where pure = V; (<*>) = ap
instance Monad Exp where
return = V
V a >>= f = f a
(x :@ y) >>= f = (x >>= f) :@ (y >>= f)
Lam e >>= f = Lam (e >>>= f)
lam :: Eq a => a > Exp a > Exp a
lam v b = Lam (abstract1 v b)
whnf :: Exp a > Exp a
whnf (f :@ a) = case whnf f of
Lam b > whnf (instantiate1 a b)
f' > f' :@ a
whnf e = e
deriveEq1 ''Exp
deriveShow1 ''Exp
main :: IO ()
main = do
let term = lam 'x' (V 'x') :@ V 'y'
print term  Lam (Scope (V (B ()))) :@ V 'y'
print $ whnf term  V 'y'
There are longer examples in the examples/ folder.
Contact Information
Contributions and bug reports are welcome!
Please feel free to contact me through github or on the #haskell IRC channel on irc.freenode.net.
Edward Kmett
Changes
2

GHC 8.0 and 8.2 support
Converted from preludeextras
to transformers
+ transformerscompat
for the Eq1
, Ord1
, Show1
, and Read1
functionality.
makeBound
supports Functor
components
Add MFunctor
instance for Scope
Add NFData
instances for Name
, Scope
, and Var
Revamp Setup.hs
to use cabaldoctest
. This makes it build
with Cabal1.25
, and makes the doctest
s work with cabal newbuild
and
sandboxes.
1.0.7
 Added an
ftemplatehaskell
option to allow disablingtemplatehaskell
support. This is an unsupported configuration but may be useful for expert users in sandbox configurations.  Support
cereal
0.5
1.0.6
Compiles warningfree on GHC 7.10
1.0.5
 Widened version bound on
bifunctors
.  Widened version bound on
profunctors
.
1.0.4
Widened version bound on
transformers
.
1.0.3
Added
bitransverseScope
.
1.0.2
Removed unneccesary constraint on
hoistScope
.
1.0.1
Added a monomorphic
hoistScope
forBound.Scope.Simple
1.0
 Added instances for
Bound
for all of themtl
monads.  Added
Data
andTypeable
support to both versions ofScope
 Added the missing
Applictive
instance toBound.Scope.Simple
 Moved
hoistScope
,bitraverseScope
,transverseScope
, andinstantiateVars
here from theermine
compiler.
0.9.1.1
Updated to work with
bifunctors
4.0
0.9.1
Updated to work with
comonad
4.0 andprofunctors
4.0
0.9
Added the missing instance for
Applicative (Scope b f)
0.8.1
SafeHaskell support
0.8
Added
Serial
,Binary
andSerialize
instances forScope
.
0.7
Added
Hashable
,Hashable1
andHashable2
instances where appropriate forName
,Var
andScope
.
0.6.1
 More aggressive inlining
 Added
unvar
,_B
,_F
toBound.Var
.  Added
_Name
toBound.Name
.
0.6
Support for
preludeextras
0.3
0.5.1
 Removed my personal interpackage dependency upper bounds
 Updated doctest suite to use exact versions.
0.5
 Created a
doctest
based test suite  Added many examples
 100% haddock coverage
 Added the
Name
Comonad
, to help retain names for bound variables.  Bumped dependencies