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

Eq (Name a)

Methods

(==) :: Name a -> Name a -> Bool

(/=) :: Name a -> Name a -> Bool

Show (Name a)

Methods

showsPrec :: Int -> Name a -> ShowS

show :: Name a -> String

showList :: [Name a] -> ShowS

NuMatching (Name a)

Methods

nuMatchingProof :: MbTypeRepr (Name a)

Show (MapRList Name c)

Methods

showsPrec :: Int -> MapRList Name c -> ShowS

show :: MapRList Name c -> String

showList :: [MapRList Name c] -> ShowS

type Binding a = Mb (RNil :> 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 one name for each type in ctx, where ctx has the form RNil :> t1 :> ... :> tn. 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 MbTypeRepr for the body type, to ensure that the names given in the pair can be relaced by fresher names.

Instances

NuMatching a => NuMatching (Mb ctx a)

Methods

nuMatchingProof :: MbTypeRepr (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.

nuMulti :: MapRList f ctx -> (MapRList 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 MapRList 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.

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

nus = nuMulti

emptyMb :: a -> Mb RNil a

Creates an empty binding that binds 0 names.

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

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

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.

Operations on multi-bindings

elimEmptyMb :: Mb RNil 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 :: MapRList any ctx2 -> Mb (ctx1 :++: ctx2) a -> Mb ctx1 (Mb ctx2 a)

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

mbToProxy :: Mb ctx a -> MapRList Proxy ctx

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

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

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

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

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

Similar to nuMultiWithElim but binds only one name.

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

Similar to nuMultiWithElim but takes only one argument

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

Similar to nuMultiWithElim but takes only one argument that binds a single name.

Orphan instances

Functor (Mb ctx)

Methods

fmap :: (a -> b) -> Mb ctx a -> Mb ctx b

(<$) :: a -> Mb ctx b -> Mb ctx a

TypeCtx ctx => Applicative (Mb ctx)

Methods

pure :: a -> Mb ctx a

(<*>) :: Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b

(*>) :: Mb ctx a -> Mb ctx b -> Mb ctx b

(<*) :: Mb ctx a -> Mb ctx b -> Mb ctx a

Show a => Show (Mb c a)

Methods

showsPrec :: Int -> Mb c a -> ShowS

show :: Mb c a -> String

showList :: [Mb c a] -> ShowS