bound-0.7: Making de Bruijn Succ Less

Portability portable experimental Edward Kmett None

Bound

Description

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 #-}
import Bound
import Control.Applicative
import Control.Monad (`ap`)
import Prelude.Extras
import Data.Foldable
import Data.Traverable
```
``` 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
instance `Ord1` Exp
instance `Show1` Exp
instance `Read1` Exp
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
```

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

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

# Manipulating user terms

substitute :: (Monad f, Eq a) => a -> f a -> f a -> f aSource

`substitute a p w` replaces the free variable `a` with `p` in `w`.

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

isClosed :: Foldable f => f a -> BoolSource

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

newtype Scope b f a Source

`Scope b f a` is an `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`.

Constructors

 Scope Fieldsunscope :: f (Var b (f a))

Instances

 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) `toList` is provides a list (with duplicates) of the free variables Traversable f => Traversable (Scope b f) (Hashable b, Monad f, Hashable1 f) => Hashable1 (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) (Hashable b, Monad f, Hashable1 f, Hashable a) => Hashable (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`

````>>> ````: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 aSource

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 aSource

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 aSource

Enter a `Scope` that binds one variable, instantiating it

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

# Structures permitting substitution

class Bound t whereSource

Instances of `Bound` may or may not be monad transformers.

If they are, then `m >>>= f ≡ m >>= lift . f` is required to hold, and is in fact the default definition. If it is not a `MonadTrans` instance, then you have greater flexibility in how to implement this class.

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.

Methods

(>>>=) :: Monad f => t f a -> (a -> f c) -> t f cSource

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`

Instances

 Bound (Scope b)

(=<<<) :: (Bound t, Monad f) => (a -> f c) -> t f a -> t f cSource

A flipped version of (`>>>=`).

`(`=<<<`) = `flip` (`>>>=`)`

# Conversion to Traditional de Bruijn

data Var b a Source

"I am not a number, I am a free monad!"

A `Var b a` is a variable that may either be "bound" (`B`) or "free" (`F`).

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

Constructors

 B b this is a bound variable F a this is a free variable

Instances

 Typeable2 Var Bitraversable Var Bifunctor Var Bifoldable Var Hashable2 Var Eq2 Var Ord2 Var Show2 Var Read2 Var Monad (Var b) Functor (Var b) Applicative (Var b) Foldable (Var b) Traversable (Var b) Hashable b => Hashable1 (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) (Data b, Data a) => Data (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) Generic (Var b a) (Hashable b, Hashable a) => Hashable (Var b a)

fromScope :: Monad f => Scope b f a -> f (Var b a)Source

`fromScope` quotients out the possible placements of `F` in `Scope` by distributing them all to the leaves. This yields a more traditional de Bruijn indexing scheme for bound variables.

Since,

``fromScope` `.` `toScope` ≡ `id``

we know that

``fromScope` `.` `toScope` `.` `fromScope` ≡ `fromScope``

and therefore `(toScope . fromScope)` is idempotent.

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