bound: Haskell 98 Locally-Nameless Generalized de Bruijn Terms

[ bsd3, compilers-interpreters, language, library ] [ Propose Tags ]

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 examples in the examples/ folder:

https://github.com/ekmett/bound/tree/master/examples

  1. 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

  2. Derived.hs shows how much of the API can be automated with DeriveTraversable and adds combinators for building binders that support pattern matching.

  3. 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.


[Skip to Readme]

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 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, 2.0.2, 2.0.3, 2.0.4, 2.0.5, 2.0.6, 2.0.7
Dependencies base (>=4 && <5), bifunctors (>=0.1.3 && <0.2), prelude-extras (>=0.2 && <0.3), 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 2012-06-17T00:03:52Z
Distributions LTSHaskell:2.0.7, NixOS:2.0.7, Stackage:2.0.7
Reverse Dependencies 9 direct, 0 indirect [details]
Downloads 36877 total (89 in the last 30 days)
Rating 2.5 (votes: 4) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs uploaded by user
Build status unknown [no reports yet]

Readme for bound-0.2

[back to package description]

Bound

Goals

This library provides convenient combinators for working with "locally-nameless" terms. These can be useful when writing a type checker, evalator, parser, or pretty printer for terms that contain binders like forall or lambda, as they ease the task of avoiding variable capture and testing for alpha-equivalence.

See the documentation on hackage for more information, but here is an example:

 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

There are longer examples in the examples/ folder.

Contact Information

Contributions and bug reports are welcome!

Please feel free to contact me through github or on the #haskell IRC channel on irc.freenode.net.

-Edward Kmett