Portability | GHC |
---|---|

Stability | experimental |

Maintainer | emw4@rice.edu |

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 (Nil :> a)
- data Mb ctx b
- nu :: (Name a -> b) -> Binding a b
- emptyMb :: a -> Mb Nil a
- nuMulti :: MapC f ctx -> (MapC Name ctx -> b) -> Mb ctx b
- elimEmptyMb :: Mb Nil a -> a
- combineMb :: Mb c1 (Mb c2 b) -> Mb (c1 :++: c2) b
- separateMb :: Append c1 c2 c -> Mb c a -> Mb c1 (Mb c2 a)
- mbToProxy :: Mb ctx a -> MapC Proxy ctx
- cmpName :: Name a -> Name b -> Maybe (a :=: b)
- mbCmpName :: Mb c (Name a) -> Mb c (Name b) -> Maybe (a :=: b)
- mbNameBoundP :: Mb ctx (Name a) -> Either (Member ctx a) (Name a)
- class Liftable a where
- class Liftable1 f where
- class Liftable2 f where
- mbList :: Mb c [a] -> [Mb c a]

# Abstract types

A `Name a`

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

.

# Multi-binding constructors

nu :: (Name a -> b) -> Binding a bSource

`nu f`

creates a binding which binds a fresh name `n`

and whose
body is the result of `f n`

.

nuMulti :: MapC f ctx -> (MapC Name ctx -> b) -> Mb ctx bSource

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

f ctx`ctx`

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

is.

# Operations on multi-bindings

elimEmptyMb :: Mb Nil a -> aSource

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

is the inverse of `emptyMb`

.

combineMb :: Mb c1 (Mb c2 b) -> Mb (c1 :++: c2) bSource

Combines a binding inside another binding into a single binding.

separateMb :: Append c1 c2 c -> Mb c a -> Mb c1 (Mb c2 a)Source

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

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

c1 c2 c`c`

should be split.

mbToProxy :: Mb ctx a -> MapC Proxy ctxSource

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

# 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

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.

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

# type classes for lifting data out of bindings

The class `Liftable a`

gives a "lifting function" for a, which can
take any data of type `a`

out of a multi-binding of type

.
`Mb`

ctx a

The class `Liftable1 f`

gives a lifting function for each type `f a`

when `a`

itself is `Liftable`

.

The class `Liftable2 f`

gives a lifting function for each type `f a b`

when `a`

and `b`

are `Liftable`

.