Copyright  (C) 2012 Edward Kmett 

License  BSDstyle (see the file LICENSE) 
Maintainer  Edward Kmett <ekmett@gmail.com> 
Stability  experimental 
Portability  portable 
Safe Haskell  None 
Language  Haskell2010 
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:
{# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, TemplateHaskell #}
import Bound
import Control.Applicative
import Control.Monad (ap
)
import Data.Functor.Classes
import Data.Foldable
import Data.Traversable
 This is from derivingcompat package
import Data.Deriving (deriveEq1, deriveOrd1, deriveRead1, deriveShow1)
infixl 9 :@ data Exp a = V a  Exp a :@ Exp a  Lam (Scope
() Exp a) deriving (Functor
,Foldable
,Traversable
)
instanceApplicative
Exp wherepure
= V; (<*>
) =ap
instanceMonad
Exp wherereturn
= V V a>>=
f = f a (x :@ y)>>=
f = (x>>=
f) :@ (y>>=
f) Lam e>>=
f = Lam (e>>>=
f)
deriveEq1 ''Exp deriveOrd1 ''Exp deriveRead1 ''Exp deriveShow1 ''Exp instanceEq
a =>Eq
(Exp a) where (==) = eq1 instanceOrd
a =>Ord
(Exp a) where compare = compare1 instanceShow
a =>Show
(Exp a) where showsPrec = showsPrec1 instanceRead
a =>Read
(Exp a) where readsPrec = readsPrec1
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.
You can also retain names in your bound variables by using Name
and the related combinators from Bound.Name. They are not reexported
from this module by default.
The approach used in this package was first elaborated upon by Richard Bird and Ross Patterson in "de Bruijn notation as a nested data type", available from http://www.cs.uwyo.edu/~jlc/courses/5000_fall_08/debruijn_as_nested_datatype.pdf
However, the combinators they used required higher rank types. Here we
demonstrate that the higher rank gfold
combinator they used isn't necessary
to build the monad and use a monad transformer to encapsulate the novel
recursion pattern in their generalized de Bruijn representation. It is named
Scope
to match up with the terminology and usage pattern from Conor McBride
and James McKinna's "I am not a number: I am a free variable", available
from http://www.cs.ru.nl/~james/RESEARCH/haskell2004.pdf, but since
the set of variables is visible in the type, we can provide stronger type
safety guarantees.
There are longer examples in the examples/
folder:
https://github.com/ekmett/bound/tree/master/examples
 Simple.hs provides an untyped lambda calculus with recursive let bindings and includes an evaluator for the untyped lambda calculus and a longer example taken from Lennart Augustsson's "λcalculus cooked four ways" available from http://foswiki.cs.uu.nl/foswiki/pub/USCS/InterestingPapers/AugustsonLambdaCalculus.pdf
 Derived.hs shows how much of the API can be automated with DeriveTraversable and adds combinators for building binders that support pattern matching.
 Overkill.hs provides very strongly typed pattern matching many modern language extensions, including polymorphic kinds to ensure type safety. In general, the approach taken by Derived seems to deliver a better power to weight ratio.
Synopsis
 substitute :: (Monad f, Eq a) => a > f a > f a > f a
 isClosed :: Foldable f => f a > Bool
 closed :: Traversable f => f a > Maybe (f b)
 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 n f a > f a
 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
 makeBound :: Name > DecsQ
Manipulating user terms
substitute :: (Monad f, Eq a) => a > f a > f a > f a Source #
replaces the free variable substitute
a p wa
with p
in w
.
>>>
substitute "hello" ["goodnight","Gracie"] ["hello","!!!"]
["goodnight","Gracie","!!!"]
isClosed :: Foldable f => f a > Bool Source #
A closed term has no free variables.
>>>
isClosed []
True
>>>
isClosed [1,2,3]
False
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.
>>>
closed [12]
Nothing
>>>
closed ""
Just []
>>>
:t closed ""
closed "" :: Maybe [b]
Scopes introduce bound variables
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
.
Instances
MonadTrans (Scope b) Source #  
Defined in Bound.Scope  
Bound (Scope b) Source #  
MFunctor (Scope b :: (Type > Type) > Type > Type) Source #  
Functor f => Generic1 (Scope b f :: Type > Type) Source #  
Monad f => Monad (Scope b f) Source #  The monad permits substitution on free variables, while preserving bound variables 
Functor f => Functor (Scope b f) Source #  
(Functor f, Monad f) => Applicative (Scope b f) Source #  
Foldable f => Foldable (Scope b f) Source # 

Defined in Bound.Scope fold :: Monoid m => Scope b f m > m # foldMap :: Monoid m => (a > m) > Scope b f a > m # foldMap' :: Monoid m => (a > m) > Scope b f a > m # foldr :: (a > b0 > b0) > b0 > Scope b f a > b0 # foldr' :: (a > b0 > b0) > b0 > Scope b f a > b0 # foldl :: (b0 > a > b0) > b0 > Scope b f a > b0 # foldl' :: (b0 > a > b0) > b0 > Scope b f a > b0 # foldr1 :: (a > a > a) > Scope b f a > a # foldl1 :: (a > a > a) > Scope b f a > a # toList :: Scope b f a > [a] # length :: Scope b f a > Int # elem :: Eq a => a > Scope b f a > Bool # maximum :: Ord a => Scope b f a > a # minimum :: Ord a => Scope b f a > a #  
Traversable f => Traversable (Scope b f) Source #  
(Monad f, Eq b, Eq1 f) => Eq1 (Scope b f) Source #  
(Monad f, Ord b, Ord1 f) => Ord1 (Scope b f) Source #  
Defined in Bound.Scope  
(Read b, Read1 f) => Read1 (Scope b f) Source #  
Defined in Bound.Scope  
(Show b, Show1 f) => Show1 (Scope b f) Source #  
(Serial b, Serial1 f) => Serial1 (Scope b f) Source #  
Defined in Bound.Scope serializeWith :: MonadPut m => (a > m ()) > Scope b f a > m () # deserializeWith :: MonadGet m => m a > m (Scope b f a) #  
(Hashable b, Monad f, Hashable1 f) => Hashable1 (Scope b f) Source #  
Defined in Bound.Scope  
(Monad f, Eq b, Eq1 f, Eq a) => Eq (Scope b f a) Source #  
(Typeable b, Typeable f, Data a, Data (f (Var b (f a)))) => Data (Scope b f a) Source #  
Defined in Bound.Scope gfoldl :: (forall d b0. Data d => c (d > b0) > d > c b0) > (forall g. g > c g) > Scope b f a > c (Scope b f a) # gunfold :: (forall b0 r. Data b0 => c (b0 > r) > c r) > (forall r. r > c r) > Constr > c (Scope b f a) # toConstr :: Scope b f a > Constr # dataTypeOf :: Scope b f a > DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) > Maybe (c (Scope b f a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) > Maybe (c (Scope b f a)) # gmapT :: (forall b0. Data b0 => b0 > b0) > Scope b f a > Scope b f a # gmapQl :: (r > r' > r) > r > (forall d. Data d => d > r') > Scope b f a > r # gmapQr :: forall r r'. (r' > r > r) > r > (forall d. Data d => d > r') > Scope b f a > r # gmapQ :: (forall d. Data d => d > u) > Scope b f a > [u] # gmapQi :: Int > (forall d. Data d => d > u) > Scope b f a > u # gmapM :: Monad m => (forall d. Data d => d > m d) > Scope b f a > m (Scope b f a) # gmapMp :: MonadPlus m => (forall d. Data d => d > m d) > Scope b f a > m (Scope b f a) # gmapMo :: MonadPlus m => (forall d. Data d => d > m d) > Scope b f a > m (Scope b f a) #  
(Monad f, Ord b, Ord1 f, Ord a) => Ord (Scope b f a) Source #  
(Read b, Read1 f, Read a) => Read (Scope b f a) Source #  
(Show b, Show1 f, Show a) => Show (Scope b f a) Source #  
Generic (Scope b f a) Source #  
(Binary b, Serial1 f, Binary a) => Binary (Scope b f a) Source #  
(Serial b, Serial1 f, Serial a) => Serial (Scope b f a) Source #  
Defined in Bound.Scope  
(Serialize b, Serial1 f, Serialize a) => Serialize (Scope b f a) Source #  
NFData (f (Var b (f a))) => NFData (Scope b f a) Source #  
Defined in Bound.Scope  
(Hashable b, Monad f, Hashable1 f, Hashable a) => Hashable (Scope b f a) Source #  
Defined in Bound.Scope  
type Rep1 (Scope b f :: Type > Type) Source #  
type Rep (Scope b f a) Source #  
Defined in Bound.Scope 
Abstraction over bound variables
abstract :: Monad f => (a > Maybe b) > f a > Scope b f a Source #
Capture some free variables in an expression to yield
a Scope
with bound variables in b
>>>
:m + Data.List
>>>
abstract (`elemIndex` "bar") "barry"
Scope [B 0,B 1,B 2,B 2,F "y"]
abstract1 :: (Monad f, Eq a) => a > f a > Scope () f a Source #
Abstract over a single variable
>>>
abstract1 'x' "xyz"
Scope [B (),F "y",F "z"]
Instantiation of bound variables
instantiate :: Monad f => (b > f a) > Scope b f a > f a Source #
Enter a scope, instantiating all bound variables
>>>
:m + Data.List
>>>
instantiate (\x > [toEnum (97 + x)]) $ abstract (`elemIndex` "bar") "barry"
"abccy"
instantiate1 :: Monad f => f a > Scope n f a > f a Source #
Enter a Scope
that binds one variable, instantiating it
>>>
instantiate1 "x" $ Scope [B (),F "y",F "z"]
"xyz"
Structures permitting substitution
Instances of Bound
generate left modules over monads.
This means they should satisfy the following laws:
m>>>=
return
≡ m m>>>=
(λ x → k x>>=
h) ≡ (m>>>=
k)>>>=
h
This guarantees that a typical Monad instance for an expression type where Bound instances appear will satisfy the Monad laws (see doc/BoundLaws.hs).
If instances of Bound
are monad transformers, then m
implies the above laws, and is in fact the default definition.>>>=
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 expressions.
Note: Free
isn't "really" a monad transformer, even if
the kind matches. Therefore there isn't
instance.Bound
Free
Nothing
(>>>=) :: Monad f => t f a > (a > f c) > t f c infixl 1 Source #
Instances
Bound ListT Source #  
Bound MaybeT Source #  
Bound (IdentityT :: (Type > Type) > Type > Type) Source #  
Error e => Bound (ErrorT e) Source #  
Bound (ReaderT r) Source #  
Bound (StateT s) Source #  
Monoid w => Bound (WriterT w) Source #  
Bound (Scope b) Source #  
Bound (Scope b) Source #  
Bound (ContT c) Source #  
Monoid w => Bound (RWST r w s) Source #  
Conversion to Traditional de Bruijn
"I am not a number, I am a free monad!"
A
is a variable that may either be "bound" (Var
b aB
) or "free" (F
).
(It is also technically a free monad in the same neartrivial sense as
Either
.)
Instances
Bitraversable Var Source #  
Defined in Bound.Var bitraverse :: Applicative f => (a > f c) > (b > f d) > Var a b > f (Var c d) #  
Bifoldable Var Source #  
Bifunctor Var Source #  
Eq2 Var Source #  
Ord2 Var Source #  
Read2 Var Source #  
Defined in Bound.Var liftReadsPrec2 :: (Int > ReadS a) > ReadS [a] > (Int > ReadS b) > ReadS [b] > Int > ReadS (Var a b) # liftReadList2 :: (Int > ReadS a) > ReadS [a] > (Int > ReadS b) > ReadS [b] > ReadS [Var a b] # liftReadPrec2 :: ReadPrec a > ReadPrec [a] > ReadPrec b > ReadPrec [b] > ReadPrec (Var a b) # liftReadListPrec2 :: ReadPrec a > ReadPrec [a] > ReadPrec b > ReadPrec [b] > ReadPrec [Var a b] #  
Show2 Var Source #  
Serial2 Var Source #  
Defined in Bound.Var serializeWith2 :: MonadPut m => (a > m ()) > (b > m ()) > Var a b > m () # deserializeWith2 :: MonadGet m => m a > m b > m (Var a b) #  
Hashable2 Var Source #  
Monad (Var b) Source #  
Functor (Var b) Source #  
Applicative (Var b) Source #  
Foldable (Var b) Source #  
Defined in Bound.Var fold :: Monoid m => Var b m > m # foldMap :: Monoid m => (a > m) > Var b a > m # foldMap' :: Monoid m => (a > m) > Var b a > m # foldr :: (a > b0 > b0) > b0 > Var b a > b0 # foldr' :: (a > b0 > b0) > b0 > Var b a > b0 # foldl :: (b0 > a > b0) > b0 > Var b a > b0 # foldl' :: (b0 > a > b0) > b0 > Var b a > b0 # foldr1 :: (a > a > a) > Var b a > a # foldl1 :: (a > a > a) > Var b a > a # elem :: Eq a => a > Var b a > Bool # maximum :: Ord a => Var b a > a # minimum :: Ord a => Var b a > a #  
Traversable (Var b) Source #  
Eq b => Eq1 (Var b) Source #  
Ord b => Ord1 (Var b) Source #  
Read b => Read1 (Var b) Source #  
Show b => Show1 (Var b) Source #  
Serial b => Serial1 (Var b) Source #  
Defined in Bound.Var serializeWith :: MonadPut m => (a > m ()) > Var b a > m () # deserializeWith :: MonadGet m => m a > m (Var b a) #  
Hashable b => Hashable1 (Var b) Source #  
Generic1 (Var b :: Type > Type) Source #  
(Eq b, Eq a) => Eq (Var b a) Source #  
(Data b, Data a) => Data (Var b a) Source #  
Defined in Bound.Var gfoldl :: (forall d b0. Data d => c (d > b0) > d > c b0) > (forall g. g > c g) > Var b a > c (Var b a) # gunfold :: (forall b0 r. Data b0 => c (b0 > r) > c r) > (forall r. r > c r) > Constr > c (Var b a) # toConstr :: Var b a > Constr # dataTypeOf :: Var b a > DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) > Maybe (c (Var b a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) > Maybe (c (Var b a)) # gmapT :: (forall b0. Data b0 => b0 > b0) > Var b a > Var b a # gmapQl :: (r > r' > r) > r > (forall d. Data d => d > r') > Var b a > r # gmapQr :: forall r r'. (r' > r > r) > r > (forall d. Data d => d > r') > Var b a > r # gmapQ :: (forall d. Data d => d > u) > Var b a > [u] # gmapQi :: Int > (forall d. Data d => d > u) > Var b a > u # gmapM :: Monad m => (forall d. Data d => d > m d) > Var b a > m (Var b a) # gmapMp :: MonadPlus m => (forall d. Data d => d > m d) > Var b a > m (Var b a) # gmapMo :: MonadPlus m => (forall d. Data d => d > m d) > Var b a > m (Var b a) #  
(Ord b, Ord a) => Ord (Var b a) Source #  
(Read b, Read a) => Read (Var b a) Source #  
(Show b, Show a) => Show (Var b a) Source #  
Generic (Var b a) Source #  
(Binary b, Binary a) => Binary (Var b a) Source #  
(Serial b, Serial a) => Serial (Var b a) Source #  
(Serialize b, Serialize a) => Serialize (Var b a) Source #  
(NFData a, NFData b) => NFData (Var b a) Source #  
(Hashable b, Hashable a) => Hashable (Var b a) Source #  
type Rep1 (Var b :: Type > Type) Source #  
Defined in Bound.Var type Rep1 (Var b :: Type > Type) = D1 ('MetaData "Var" "Bound.Var" "bound2.0.3IMm1RxjoHWu6bB6DEZNDCu" 'False) (C1 ('MetaCons "B" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 b)) :+: C1 ('MetaCons "F" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) Par1))  
type Rep (Var b a) Source #  
Defined in Bound.Var type Rep (Var b a) = D1 ('MetaData "Var" "Bound.Var" "bound2.0.3IMm1RxjoHWu6bB6DEZNDCu" 'False) (C1 ('MetaCons "B" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 b)) :+: C1 ('MetaCons "F" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a))) 
toScope :: Monad f => f (Var b a) > Scope b f a Source #
Convert from traditional de Bruijn to generalized de Bruijn indices.
This requires a full tree traversal
Deriving instances
makeBound :: Name > DecsQ Source #
Use to automatically derive Applicative
and Monad
instances for
your datatype.
Also works for components that are lists or instances of Functor
,
but still does not work for a great deal of other things.
derivingcompat
package may be used to derive the Show1
and Read1
instances
{# LANGUAGE DeriveFunctor #} {# LANGUAGE TemplateHaskell #} import Bound (Scope, makeBound) import Data.Functor.Classes (Show1, Read1, showsPrec1, readsPrec1) import Data.Deriving (deriveShow1, deriveRead1) data Exp a = V a  App (Exp a) (Exp a)  Lam (Scope () Exp a)  ND [Exp a]  I Int deriving (Functor) makeBound ''Exp deriveShow1 ''Exp deriveRead1 ''Exp instance Read a => Read (Exp a) where readsPrec = readsPrec1 instance Show a => Show (Exp a) where showsPrec = showsPrec1
and in GHCi
ghci> :set XDeriveFunctor ghci> :set XTemplateHaskell ghci> import Bound (Scope, makeBound) ghci> import Data.Functor.Classes (Show1, Read1, showsPrec1, readsPrec1) ghci> import Data.Deriving (deriveShow1, deriveRead1) ghci> :{ ghci data Exp a = V a  App (Exp a) (Exp a)  Lam (Scope () Exp a)  ND [Exp a]  I Int deriving (Functor) ghci makeBound ''Exp ghci deriveShow1 ''Exp ghci deriveRead1 ''Exp ghci instance Read a => Read (Exp a) where readsPrec = readsPrec1 ghci instance Show a => Show (Exp a) where showsPrec = showsPrec1 ghci :}
Eq
and Ord
instances can be derived similarly
import Data.Functor.Classes (Eq1, Ord1, eq1, compare1) import Data.Deriving (deriveEq1, deriveOrd1) deriveEq1 ''Exp deriveOrd1 ''Exp instance Eq a => Eq (Exp a) where (==) = eq1 instance Ord a => Ord (Exp a) where compare = compare1
or in GHCi:
ghci> import Data.Functor.Classes (Eq1, Ord1, eq1, compare1) ghci> import Data.Deriving (deriveEq1, deriveOrd1) ghci> :{ ghci deriveEq1 ''Exp ghci deriveOrd1 ''Exp ghci instance Eq a => Eq (Exp a) where (==) = eq1 ghci instance Ord a => Ord (Exp a) where compare = compare1 ghci :}
We cannot automatically derive Eq
and Ord
using the standard GHC mechanism,
because instances require Exp
to be a Monad
:
instance (Monad f, Eq b, Eq1 f, Eq a) => Eq (Scope b f a) instance (Monad f, Ord b, Ord1 f, Ord a) => Ord (Scope b f a)