Copyright | (c) 2011 Edwin Westbrook Nicolas Frisby and Paul Brauner |
---|---|

License | BSD3 |

Maintainer | emw4@rice.edu |

Stability | experimental |

Portability | GHC |

Safe Haskell | None |

Language | Haskell98 |

This module defines multi-bindings as the type `Mb`

, as well as a number of
operations on multi-bindings. See the paper E. Westbrook, N. Frisby,
P. Brauner, "Hobbits for Haskell: A Library for Higher-Order Encodings in
Functional Programming Languages" for more information.

- data Name a
- type Binding a = Mb (RNil :> a)
- data Mb ctx b
- nu :: (Name a -> b) -> Binding a b
- nuMulti :: MapRList f ctx -> (MapRList Name ctx -> b) -> Mb ctx b
- nus :: MapRList f ctx -> (MapRList Name ctx -> b) -> Mb ctx b
- emptyMb :: a -> Mb RNil a
- cmpName :: Name a -> Name b -> Maybe (a :~: b)
- mbNameBoundP :: Mb ctx (Name a) -> Either (Member ctx a) (Name a)
- mbCmpName :: Mb c (Name a) -> Mb c (Name b) -> Maybe (a :~: b)
- elimEmptyMb :: Mb RNil a -> a
- mbCombine :: Mb c1 (Mb c2 b) -> Mb (c1 :++: c2) b
- mbSeparate :: MapRList any ctx2 -> Mb (ctx1 :++: ctx2) a -> Mb ctx1 (Mb ctx2 a)
- mbToProxy :: Mb ctx a -> MapRList Proxy ctx
- mbSwap :: Mb ctx1 (Mb ctx2 a) -> Mb ctx2 (Mb ctx1 a)
- mbApply :: Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
- nuMultiWithElim :: TypeCtx ctx => (MapRList Name ctx -> MapRList Identity args -> b) -> MapRList (Mb ctx) args -> Mb ctx b
- nuWithElim :: (Name a -> MapRList Identity args -> b) -> MapRList (Mb (RNil :> a)) args -> Binding a b
- nuMultiWithElim1 :: TypeCtx ctx => (MapRList Name ctx -> arg -> b) -> Mb ctx arg -> Mb ctx b
- nuWithElim1 :: (Name a -> arg -> b) -> Binding a arg -> Binding a b

# Abstract types

A `Name a`

is a bound name that is associated with type `a`

.

An `Mb ctx b`

is a multi-binding that binds one name for each type
in `ctx`

, where `ctx`

has the form

.
Internally, multi-bindings are represented either as "fresh
functions", which are functions that quantify over all fresh names
that have not been used before and map them to the body of the
binding, or as "fresh pairs", which are pairs of a list of names
that are guaranteed to be fresh along with a body. Note that fresh
pairs must come with an `RNil`

`:>`

t1 `:>`

... `:>`

tn`MbTypeRepr`

for the body type, to ensure
that the names given in the pair can be relaced by fresher names.

NuMatching a => NuMatching (Mb ctx a) Source # | |

# Multi-binding constructors

nu :: (Name a -> b) -> Binding a b Source #

`nu f`

creates a binding which binds a fresh name `n`

and whose
body is the result of `f n`

.

nuMulti :: MapRList f ctx -> (MapRList Name ctx -> b) -> Mb ctx b Source #

The expression `nuMulti p f`

creates a multi-binding of zero or more
names, one for each element of the vector `p`

. The bound names are
passed the names to `f`

, which returns the body of the
multi-binding. The argument `p`

, of type

, acts as a
"phantom" argument, used to reify the list of types `MapRList`

f ctx`ctx`

at the
term level; thus it is unimportant what the type function `f`

is.

# Queries on names

cmpName :: Name a -> Name b -> Maybe (a :~: b) Source #

`cmpName n m`

compares names `n`

and `m`

of types `Name a`

and `Name b`

,
respectively. When they are equal, `Some e`

is returned for `e`

a proof
of type `a :~: b`

that their types are equal. Otherwise, `None`

is returned.

For example:

nu $ \n -> nu $ \m -> cmpName n n == nu $ \n -> nu $ \m -> Some Refl nu $ \n -> nu $ \m -> cmpName n m == nu $ \n -> nu $ \m -> None

mbNameBoundP :: Mb ctx (Name a) -> Either (Member ctx a) (Name a) Source #

Checks if a name is bound in a multi-binding, returning `Left mem`

when the name is bound, where `mem`

is a proof that the type of the
name is in the type list for the multi-binding, and returning
`Right n`

when the name is not bound, where `n`

is the name.

For example:

nu $ \n -> mbNameBoundP (nu $ \m -> m) == nu $ \n -> Left Member_Base nu $ \n -> mbNameBoundP (nu $ \m -> n) == nu $ \n -> Right n

mbCmpName :: Mb c (Name a) -> Mb c (Name b) -> Maybe (a :~: b) Source #

Compares two names inside bindings, taking alpha-equivalence into
account; i.e., if both are the `i`

th name, or both are the same name
not bound in their respective multi-bindings, then they compare as
equal. The return values are the same as for `cmpName`

, so that
`Some Refl`

is returned when the names are equal and `Nothing`

is
returned when they are not.

# Operations on multi-bindings

elimEmptyMb :: Mb RNil a -> a Source #

Eliminates an empty binding, returning its body. Note that
`elimEmptyMb`

is the inverse of `emptyMb`

.

mbCombine :: Mb c1 (Mb c2 b) -> Mb (c1 :++: c2) b Source #

Combines a binding inside another binding into a single binding.

mbSeparate :: MapRList any ctx2 -> Mb (ctx1 :++: ctx2) a -> Mb ctx1 (Mb ctx2 a) Source #

Separates a binding into two nested bindings. The first argument, of
type

, is a "phantom" argument to indicate how
the context `MapRList`

any c2`c`

should be split.

mbToProxy :: Mb ctx a -> MapRList Proxy ctx Source #

Returns a proxy object that enumerates all the types in ctx.

mbSwap :: Mb ctx1 (Mb ctx2 a) -> Mb ctx2 (Mb ctx1 a) Source #

Take a multi-binding inside another multi-binding and move the outer binding inside the ineer one.

mbApply :: Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b Source #

Applies a function in a multi-binding to an argument in a multi-binding that binds the same number and types of names.

# Eliminators for multi-bindings

nuMultiWithElim :: TypeCtx ctx => (MapRList Name ctx -> MapRList Identity args -> b) -> MapRList (Mb ctx) args -> Mb ctx b Source #

The expression `nuWithElimMulti args f`

takes a sequence `args`

of
zero or more multi-bindings, each of type `Mb ctx ai`

for the same
type context `ctx`

of bound names, and a function `f`

and does the
following:

- Creates a multi-binding that binds names
`n1,...,nn`

, one name for each type in`ctx`

; - Substitutes the names
`n1,...,nn`

for the names bound by each argument in the`args`

sequence, yielding the bodies of the`args`

(using the new name`n`

); and then - Passes the sequence
`n1,...,nn`

along with the result of substituting into`args`

to the function`f`

, which then returns the value for the newly created binding.

Note that the types in `args`

must each have a `NuMatching`

instance;
this is represented with the `NuMatchingList`

type class.

Here are some examples:

(<*>) :: Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b (<*>) f a = nuWithElimMulti ('MNil' :>: f :>: a) (\_ ('MNil' :>: 'Identity' f' :>: 'Identity' a') -> f' a')

nuWithElim :: (Name a -> MapRList Identity args -> b) -> MapRList (Mb (RNil :> a)) args -> Binding a b Source #

Similar to `nuMultiWithElim`

but binds only one name.

nuMultiWithElim1 :: TypeCtx ctx => (MapRList Name ctx -> arg -> b) -> Mb ctx arg -> Mb ctx b Source #

Similar to `nuMultiWithElim`

but takes only one argument

nuWithElim1 :: (Name a -> arg -> b) -> Binding a arg -> Binding a b Source #

Similar to `nuMultiWithElim`

but takes only one argument that binds
a single name.