Portability  portable 

Stability  experimental 
Maintainer  Edward Kmett <ekmett@gmail.com> 
Safe Haskell  SafeInfered 
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
 newtype Scope b f a = Scope {}
 abstract :: Monad f => (a > Maybe b) > f a > Scope b f a
 abstract1 :: (Monad f, Eq a) => a > f a > Scope () f a
 instantiate :: Monad f => (b > f a) > Scope b f a > f a
 instantiate1 :: Monad f => f a > Scope () f a > f a
 substitute :: (Monad f, Eq a) => f a > a > f a > f a
 isClosed :: Foldable f => f a > Bool
 closed :: Traversable f => f a > Maybe (f b)
 class Bound t where
 (=<<<) :: (Bound t, Monad f) => (a > f c) > t f a > t f c
 data Var b a
 fromScope :: Monad f => Scope b f a > f (Var b a)
 toScope :: Monad f => f (Var b a) > Scope b f a
 splat :: Monad f => (a > f c) > (b > f c) > Scope b f a > f c
 mapBound :: Functor f => (b > b') > Scope b f a > Scope b' f a
 mapScope :: Functor f => (b > d) > (a > c) > Scope b f a > Scope d f c
 liftMBound :: Monad m => (b > b') > Scope b m a > Scope b' m a
 liftMScope :: Monad m => (b > d) > (a > c) > Scope b m a > Scope d m c
 foldMapBound :: (Foldable f, Monoid r) => (b > r) > Scope b f a > r
 foldMapScope :: (Foldable f, Monoid r) => (b > r) > (a > r) > Scope b f a > r
 traverseBound_ :: (Applicative g, Foldable f) => (b > g d) > Scope b f a > g ()
 traverseScope_ :: (Applicative g, Foldable f) => (b > g d) > (a > g c) > Scope b f a > g ()
 mapMBound_ :: (Monad g, Foldable f) => (b > g d) > Scope b f a > g ()
 mapMScope_ :: (Monad m, Foldable f) => (b > m d) > (a > m c) > Scope b f a > m ()
 traverseBound :: (Applicative g, Traversable f) => (b > g c) > Scope b f a > g (Scope c f a)
 traverseScope :: (Applicative g, Traversable f) => (b > g d) > (a > g c) > Scope b f a > g (Scope d f c)
 mapMBound :: (Monad m, Traversable f) => (b > m c) > Scope b f a > m (Scope c f a)
 mapMScope :: (Monad m, Traversable f) => (b > m d) > (a > m c) > Scope b f a > m (Scope d f c)
Scopes introduce bound variables in user terms
is an Scope
b f af
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
.
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) 

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
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
Combinators for manipulating user terms
substitute :: (Monad f, Eq a) => f a > a > f a > f aSource
replaces the free variable substitute
p a wa
with p
in w
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.
Structures permitting substitution
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.
Conversion to Traditional de Bruijn
"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
.)
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) 
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
Advanced substitution combinators
splat :: Monad f => (a > f c) > (b > f c) > Scope b f a > f cSource
Perform substitution on both bound and free variables in a Scope
mapBound :: Functor f => (b > b') > Scope b f a > Scope b' f aSource
Perform a change of variables on bound variables
mapScope :: Functor f => (b > d) > (a > c) > Scope b f a > Scope d f cSource
Perform a change of variables, reassigning both bound and free variables.
liftMBound :: Monad m => (b > b') > Scope b m a > Scope b' m aSource
Perform a change of variables on bound variables given only a Monad
instance
liftMScope :: Monad m => (b > d) > (a > c) > Scope b m a > Scope d m cSource
foldMapBound :: (Foldable f, Monoid r) => (b > r) > Scope b f a > rSource
Obtain a result by collecting information from both bound and free variables
foldMapScope :: (Foldable f, Monoid r) => (b > r) > (a > r) > Scope b f a > rSource
Obtain a result by collecting information from both bound and free variables
traverseBound_ :: (Applicative g, Foldable f) => (b > g d) > Scope b f a > g ()Source
traverseScope_ :: (Applicative g, Foldable f) => (b > g d) > (a > g c) > Scope b f a > g ()Source
mapMBound_ :: (Monad g, Foldable f) => (b > g d) > Scope b f a > g ()Source
mapM_ over the variables bound by this scope
mapMScope_ :: (Monad m, Foldable f) => (b > m d) > (a > m c) > Scope b f a > m ()Source
A traverseScope_
that can be used when you only have a Monad
instance
traverseBound :: (Applicative g, Traversable f) => (b > g c) > Scope b f a > g (Scope c f a)Source
traverseScope :: (Applicative g, Traversable f) => (b > g d) > (a > g c) > Scope b f a > g (Scope d f c)Source