hobbits-1.0: A library for canonically representing terms with binding





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 Source

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


type Binding a = Mb (Nil :> a)Source

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

data Mb ctx b Source

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.


Typeable2 Mb 
Show a => Show (Mb c a) 
NuElim a => NuElim (Mb ctx 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.

emptyMb :: a -> Mb Nil aSource

Creates an empty binding that binds 0 names.

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 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 -> 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 Append c1 c2 c, is a "phantom" argument to indicate how the context 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 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)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

class Liftable a whereSource

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.


mbLift :: Mb ctx a -> aSource


class Liftable1 f whereSource

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


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


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

class Liftable2 f whereSource

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


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

Optimized, safe multi-binding eliminators

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

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