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

Portability portable experimental Edward Kmett Safe-Infered

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:

``` import Bound
import Prelude.Extras
```
``` infixl 9 :@
data Exp a = V a | Exp a :@ Exp a | Lam (Scope () Exp a)
```
``` instance Eq1 Exp   where (==#)      = (==)
instance Ord1 Exp  where compare1   = compare
instance Show1 Exp where showsPrec1 = showsPrec
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
```

Synopsis

# Scopes introduce bound variables in user terms

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

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

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

Abstract over a single variable

## Instantiation of bound variables

instantiate :: Monad f => (b -> f a) -> Scope b f a -> f aSource

Enter a scope, instantiating all bound variables

instantiate1 :: Monad f => f a -> Scope () f a -> f aSource

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

# Combinators for manipulating user terms

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

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

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 uses

# Structures permitting substitution

class Bound t whereSource

Instantces may or may not be monad transformers.

If they are, then you can use `m >>>= 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 one.

Methods

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

Instances

 Bound (Scope b)

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

## Conversion to Traditional de Bruijn

data Var b a Source

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

`Var b a` represents variables 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 F a

Instances

 Bitraversable Var Bifunctor Var Bifoldable Var Eq2 Var Ord2 Var Show2 Var Read2 Var Monad (Var b) Functor (Var b) Applicative (Var b) Foldable (Var b) Traversable (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) (Ord b, Ord a) => Ord (Var b a) (Read b, Read a) => Read (Var b a) (Show b, Show a) => Show (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.

``` fromScope . toScope = id
fromScope . toScope . fromScope = fromScope
```

`(toScope . fromScope)` is idempotent

toScope :: Monad f => f (Var b a) -> Scope b f aSource

splat :: Monad f => (a -> f c) -> (b -> f c) -> Scope b f a -> f cSource

Perform substitution on both bound and free variables in a `Scope`

mapBound :: Functor f => (b -> b') -> Scope b f a -> Scope b' f aSource

Perform a change of variables on bound variables

mapScope :: Functor f => (b -> d) -> (a -> c) -> Scope b f a -> Scope d f cSource

Perform a change of variables, reassigning both bound and free variables.

liftMBound :: Monad m => (b -> b') -> Scope b m a -> Scope b' m aSource

Perform a change of variables on bound variables given only a `Monad` instance

liftMScope :: Monad m => (b -> d) -> (a -> c) -> Scope b m a -> Scope d m cSource

A version of `mapScope` that can be used when you only have the `Monad` instance

foldMapBound :: (Foldable f, Monoid r) => (b -> r) -> Scope b f a -> rSource

Obtain a result by collecting information from both bound and free variables

foldMapScope :: (Foldable f, Monoid r) => (b -> r) -> (a -> r) -> Scope b f a -> rSource

Obtain a result by collecting information from both bound and free variables

traverseBound_ :: (Applicative g, Foldable f) => (b -> g d) -> Scope b f a -> g ()Source

traverseScope_ :: (Applicative g, Foldable f) => (b -> g d) -> (a -> g c) -> Scope b f a -> g ()Source

mapMBound_ :: (Monad g, Foldable f) => (b -> g d) -> Scope b f a -> g ()Source

mapM_ over the variables bound by this scope

mapMScope_ :: (Monad m, Foldable f) => (b -> m d) -> (a -> m c) -> Scope b f a -> m ()Source

traverseBound :: (Applicative g, Traversable f) => (b -> g c) -> Scope b f a -> g (Scope c f a)Source

traverseScope :: (Applicative g, Traversable f) => (b -> g d) -> (a -> g c) -> Scope b f a -> g (Scope d f c)Source

mapMBound :: (Monad m, Traversable f) => (b -> m c) -> Scope b f a -> m (Scope c f a)Source

mapMScope :: (Monad m, Traversable f) => (b -> m d) -> (a -> m c) -> Scope b f a -> m (Scope d f c)Source