Copyright | (C) 2012 Edward Kmett |
---|---|

License | BSD-style (see the file LICENSE) |

Maintainer | Edward Kmett <ekmett@gmail.com> |

Stability | experimental |

Portability | portable |

Safe Haskell | None |

Language | Haskell98 |

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 deriving-compat 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`

)

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)

deriveEq1 ''Exp deriveOrd1 ''Exp deriveRead1 ''Exp deriveShow1 ''Exp instance`Eq`

a =>`Eq`

(Exp a) where (==) = eq1 instance`Ord`

a =>`Ord`

(Exp a) where compare = compare1 instance`Show`

a =>`Show`

(Exp a) where showsPrec = showsPrec1 instance`Read`

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 re-exported
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.

- 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 w`a`

with `p`

in `w`

.

`>>>`

["goodnight","Gracie","!!!"]`substitute "hello" ["goodnight","Gracie"] ["hello","!!!"]`

isClosed :: Foldable f => f a -> Bool Source #

A closed term has no free variables.

`>>>`

True`isClosed []`

`>>>`

False`isClosed [1,2,3]`

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.

`>>>`

Nothing`closed [12]`

`>>>`

Just []`closed ""`

`>>>`

closed "" :: Maybe [b]`:t closed ""`

# Scopes introduce bound variables

is an `Scope`

b f a`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`

.

## 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`

`>>>`

Scope [B 0,B 1,B 2,B 2,F "y"]`abstract (`elemIndex` "bar") "barry"`

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

Abstract over a single variable

`>>>`

Scope [B (),F "y",F "z"]`abstract1 'x' "xyz"`

## 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`

`>>>`

"abccy"`instantiate (\x -> [toEnum (97 + x)]) $ abstract (`elemIndex` "bar") "barry"`

instantiate1 :: Monad f => f a -> Scope n f a -> f a Source #

Enter a `Scope`

that binds one variable, instantiating it

`>>>`

"xyz"`instantiate1 "x" $ Scope [B (),F "y",F "z"]`

# 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`

(>>>=) :: Monad f => t f a -> (a -> f c) -> t f c infixl 1 Source #

Perform substitution

If `t`

is an instance of `MonadTrans`

and you are compiling on GHC >= 7.4, then this
gets the default definition:

m`>>>=`

f = m`>>=`

`lift`

`.`

f

(>>>=) :: (MonadTrans t, Monad f, Monad (t f)) => t f a -> (a -> f c) -> t f c infixl 1 Source #

Bound ListT Source # | |

Bound MaybeT Source # | |

Bound (IdentityT *) Source # | |

Error e => Bound (ErrorT e) Source # | |

Bound (StateT s) Source # | |

Monoid w => Bound (WriterT w) Source # | |

Bound (Scope b) Source # | |

Bound (Scope b) Source # | |

Bound (ContT * c) Source # | |

Bound (ReaderT * r) 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 a`B`

) or "free" (`F`

).

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

.)

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.

`deriving-compat`

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, shosPrec1, 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)