bound: Making de Bruijn Succ Less

[ bsd3, compilers-interpreters, language, library ] [ Propose Tags ]
Versions 0.1, 0.1.1, 0.1.2, 0.1.3, 0.1.4, 0.2, 0.2.1, 0.3.1, 0.3.2, 0.4, 0.5,,, 0.5.1, 0.6, 0.6.1, 0.7, 0.8, 0.8.1, 0.9,, 0.9.1,, 1.0, 1.0.1, 1.0.2, 1.0.3, 1.0.4, 1.0.5, 1.0.6, 1.0.7, 2, 2.0.1
Change log CHANGELOG.markdown
Dependencies base (==4.*), bifunctors (==3.0.*), comonad (==3.0.*), ghc‑prim, prelude‑extras (==0.2.*), transformers (>=0.2 && <0.4) [details]
License BSD-3-Clause
Copyright Copyright (C) 2012 Edward A. Kmett
Author Edward A. Kmett
Maintainer Edward A. Kmett <>
Category Language, Compilers/Interpreters
Home page
Bug tracker
Source repo head: git clone git://
Uploaded by EdwardKmett at Thu Sep 13 20:40:21 UTC 2012
Distributions LTSHaskell:2.0.1, NixOS:2.0.1, Stackage:2.0.1, openSUSE:2.0.1
Downloads 14003 total (109 in the last 30 days)
Rating 2.5 (votes: 4) [estimated by rule of succession]
Your Rating
  • λ
  • λ
  • λ
Status Docs uploaded by user
Build status unknown [no reports yet]
Hackage Matrix CI

We represent the target language itself as an ideal monad supplied by the user, and provide a Scope monad transformer for introducing bound variables in user supplied terms. Users supply a Monad and Traversable instance, and we traverse to find free variables, and use the Monad to perform substitution that avoids bound variables.

Slides describing and motivating this approach to name binding are available online at:

The goal of this package is to make it as easy as possible to deal with name binding without forcing an awkward monadic style on the user.

With generalized de Bruijn term you can lift whole trees instead of just applying succ to individual variables, weakening the all variables bound by a scope and greatly speeding up instantiation. By giving binders more structure we permit easy simultaneous substitution and further speed up instantiation.

[Skip to Readme]




Maintainer's Corner

For package maintainers and hackage trustees

Readme for bound-

[back to package description]


Build Status


This library provides convenient combinators for working with "locally-nameless" terms. These can be useful when writing a type checker, evalator, 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 alpha-equivalence.

See the documentation on hackage for more information, but here is an example:

 import Bound
 import Prelude.Extras

 infixl 9 :@
 data Exp a = V a | Exp a :@ Exp a | Lam (Scope () Exp a)
   deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)

 instance Eq1 Exp   where (==#)      = (==)
 instance Ord1 Exp  where compare1   = compare
 instance Show1 Exp where showsPrec1 = showsPrec
 instance Read1 Exp where readsPrec1 = readsPrec
 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

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

-Edward Kmett