Data.Binding.Hobbits.Mb

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.

Abstract types

data Name a

A Name a is a bound name that is associated with type a.

Instances

Typeable1 Name

Eq (Name a)

Show (Name a)

NuElim (Name a)

Show (MapC Name c)

type Binding a = Mb (Nil :> a)

A Binding is simply a multi-binding that binds one name

data Mb ctx b

An Mb ctx b is a multi-binding that binds exactly one name for each type in ctx, where ctx has the form Nil :> t1 :> ... :> tn.

Instances

Typeable2 Mb

Show a => Show (Mb c a)

NuElim a => NuElim (Mb ctx a)

Multi-binding constructors

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

nu f creates a binding which binds a fresh name n and whose body is the result of f n.

emptyMb :: a -> Mb Nil a

Creates an empty binding that binds 0 names.

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

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 Mb f ctx, acts as a "phantom" argument, used to reify the list of types ctx at the term level; thus it is unimportant what the type function f is.

Operations on multi-bindings

elimEmptyMb :: Mb Nil a -> a

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

Combines a binding inside another binding into a single binding.

mbSeparate :: Append c1 c2 c -> Mb c a -> Mb c1 (Mb c2 a)

Separates a binding into two nested bindings. The first argument, of type Append c1 c2 c, is a "phantom" argument to indicate how the context c should be split.

mbToProxy :: Mb ctx a -> MapC Proxy ctx

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

Queries on names

cmpName :: Name a -> Name b -> Maybe (a :=: b)

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)

Compares two names inside bindings, taking alpha-equivalence into account; i.e., if both are the ith 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)

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

class Liftable a where

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.

Methods

mbLift :: Mb ctx a -> a

Instances

Liftable Char

Liftable Int

(Liftable1 f, Liftable a) => Liftable (f a)

Liftable (Member c a)

class Liftable1 f where

The class Liftable1 f gives a lifting function for each type f a when a itself is Liftable.

Methods

mbLift1 :: Liftable a => Mb ctx (f a) -> f a

Instances

Liftable1 []

(Liftable2 f, Liftable a) => Liftable1 (f a)

class Liftable2 f where

The class Liftable2 f gives a lifting function for each type f a b when a and b are Liftable.

Methods

mbLift2 :: (Liftable a, Liftable b) => Mb ctx (f a b) -> f a b

Optimized, safe multi-binding eliminators

mbList :: Mb c [a] -> [Mb c a]

Lift a list (but not its elements) out of a multi-binding

Synonyms

nus :: MapC f ctx -> (MapC Name ctx -> b) -> Mb ctx b

nus = nuMulti