bound-0.4: Haskell 98/2010 Locally-Nameless Generalized de Bruijn Terms

MaintainerEdward Kmett <>
Safe HaskellSafe-Infered




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.

An untyped lambda calculus:

 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

More exotic combinators for manipulating a Scope can be imported from Bound.Scope.


Manipulating user terms

substitute :: (Monad f, Eq a) => a -> f a -> f a -> f aSource

substitute a p w replaces the free variable a with p in w

isClosed :: Foldable f => f a -> BoolSource

A closed term has no free variables.

closed :: Traversable f => f a -> Maybe (f b)Source

If a term has no free variables, you can freely change the type of free variables it is parameterized on.

Scopes introduce bound variables

newtype Scope b f a Source

Scope b f a is an f expression with bound variables in b, and free variables in a

We store bound variables as their generalized de Bruijn representation in that we're allowed to lift (using F) an entire tree rather than only succ individual variables, but we're still only allowed to do so once per Scope. Weakening trees permits O(1) weakening and permits more sharing opportunities. Here the deBruijn 0 is represented by the B constructor of Var, while the de Bruijn succ (which may be applied to an entire tree!) is handled by F.

NB: equality and comparison quotient out the distinct F placements allowed by the generalized de Bruijn representation and return the same result as a traditional de Bruijn representation would.

Logically you can think of this as if the shape were the traditional f (Var b a), but the extra f a inside permits us a cheaper lift.




unscope :: f (Var b (f a))


MonadTrans (Scope b) 
Bound (Scope b) 
Monad f => Monad (Scope b f)

The monad permits substitution on free variables, while preserving bound variables

Functor f => Functor (Scope b f) 
Foldable f => Foldable (Scope b f)

toList is provides a list (with duplicates) of the free variables

Traversable f => Traversable (Scope b f) 
(Monad f, Eq b, Eq1 f) => Eq1 (Scope b f) 
(Monad f, Ord b, Ord1 f) => Ord1 (Scope b f) 
(Functor f, Show b, Show1 f) => Show1 (Scope b f) 
(Functor f, Read b, Read1 f) => Read1 (Scope b f) 
(Monad f, Eq b, Eq1 f, Eq a) => Eq (Scope b f a) 
(Monad f, Ord b, Ord1 f, Ord a) => Ord (Scope b f a) 
(Functor f, Read b, Read1 f, Read a) => Read (Scope b f a) 
(Functor f, Show b, Show1 f, Show a) => Show (Scope b f a) 

Abstraction over bound variables

abstract :: Monad f => (a -> Maybe b) -> f a -> Scope b f aSource

Capture some free variables in an expression to yield a Scope with bound variables in b

abstract1 :: (Monad f, Eq a) => a -> f a -> Scope () f aSource

Abstract over a single variable

Instantiation of bound variables

instantiate :: Monad f => (b -> f a) -> Scope b f a -> f aSource

Enter a scope, instantiating all bound variables

instantiate1 :: Monad f => f a -> Scope () f a -> f aSource

Enter a Scope that binds one variable, instantiating it

Structures permitting substitution

class Bound t whereSource

Instances may or may not be monad transformers.

If they are, then you can use m >>>= f = m >>= lift . f

This is useful for types like expression lists, case alternatives, schemas, etc. that may not be expressions in their own right, but often contain one.


(>>>=) :: Monad f => t f a -> (a -> f c) -> t f cSource


Bound (Scope b) 

(=<<<) :: (Bound t, Monad f) => (a -> f c) -> t f a -> t f cSource

Conversion to Traditional de Bruijn

data Var b a Source

"I am not a number, I am a free monad!"

A Var b a is a variable that may either be "bound" or "free".

(It is also technically a free monad in the same near trivial sense as Either.)


B b

this is a bound variable

F a

this is a free variable


Bitraversable Var 
Bifunctor Var 
Bifoldable Var 
Eq2 Var 
Ord2 Var 
Show2 Var 
Read2 Var 
Monad (Var b) 
Functor (Var b) 
Applicative (Var b) 
Foldable (Var b) 
Traversable (Var b) 
Eq b => Eq1 (Var b) 
Ord b => Ord1 (Var b) 
Show b => Show1 (Var b) 
Read b => Read1 (Var b) 
(Eq b, Eq a) => Eq (Var b a) 
(Ord b, Ord a) => Ord (Var b a) 
(Read b, Read a) => Read (Var b a) 
(Show b, Show a) => Show (Var b a) 

fromScope :: Monad f => Scope b f a -> f (Var b a)Source

fromScope quotients out the possible placements of F in Scope by distributing them all to the leaves. This yields a more traditional de Bruijn indexing scheme for bound variables.

 fromScope . toScope = id
 fromScope . toScope . fromScope = fromScope

(toScope . fromScope) is idempotent

toScope :: Monad f => f (Var b a) -> Scope b f aSource

Convert from traditional de Bruijn to generalized de Bruijn indices.

This requires a full tree traversal