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

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

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.

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

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 RAssign 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 = nuMulti

Creates an empty binding that binds 0 names.

Extend the context of a name-binding by adding a single type

Extend the context of a name-binding with multiple types

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

Heterogeneous comparison of names, that could be at different kinds

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

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.

Eliminates an empty binding, returning its body. Note that elimEmptyMb is the inverse of emptyMb.

Combines a binding inside another binding into a single binding.

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

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

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

Put a value inside a multi-binding

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

Lift a binary function function to Mbs

asdfasdf

The expression nuWithElimMulti args f takes a sequence args of one or more multi-bindings (it is a runtime error to pass an empty sequence of arguments), 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.

For example, here is an alternate way to implement mbApply:

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

Similar to nuMultiWithElim but binds only one name. Note that the argument list here is allowed to be empty.

Similar to nuMultiWithElim but takes only one argument

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