# bound: Haskell 98 Locally-Nameless Generalized de Bruijn Terms

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

The classes from Prelude.Extras are used to facilitate the automatic deriving
of `Eq`

, `Ord`

, 'Show, and `Read`

in the presence of polymorphic recursion used
inside `Scope`

.

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 by giving binders more structure we can permit easy
simultaneous substitution.

The approach 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.st-andrews.ac.uk/~james/RESEARCH/notanum.pdf, but since the
set of variables is visible in the type, we can provide stronger type safety
guarantees.

There are longer worked 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://www.augustsson.net/Darcs/Lambda/top.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 type extensions, including polymorphic kinds to ensure type safety. In general, the approach taken by Derived seems to deliver a better power to weight ratio.

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.0.1, 0.5.0.2, 0.5.1, 0.6, 0.6.1, 0.7, 0.8, 0.8.1, 0.9, 0.9.0.1, 0.9.1, 0.9.1.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 |
---|---|

Dependencies | base (==4.*), bifunctors (>=0.1.3 && <0.2), 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 <ekmett@gmail.com> |

Category | Language, Compilers/Interpreters |

Home page | http://github.com/ekmett/bound/ |

Bug tracker | http://github.com/ekmett/bound/issues |

Source repo | head: git clone git://github.com/ekmett/bound.git |

Uploaded | by EdwardKmett at Sat Jun 16 23:51:19 UTC 2012 |

Distributions | LTSHaskell:2.0.1, NixOS:2.0.1, Stackage:2.0.1 |

Downloads | 14656 total (343 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 |

## Downloads

- bound-0.1.4.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)