Portability | GHC |
---|---|
Stability | experimental |
Maintainer | emw4@rice.edu |
Safe Haskell | None |
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
- mbCombine :: Mb c1 (Mb c2 b) -> Mb (c1 :++: c2) b
- mbSeparate :: 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)
- mbLiftChar :: Mb c Char -> Char
- mbLiftInt :: Mb c Int -> Int
- mbLiftInteger :: Mb c Integer -> Integer
- nus :: MapC f ctx -> (MapC Name ctx -> b) -> Mb ctx b
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 ctxctx
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
.
mbCombine :: Mb c1 (Mb c2 b) -> Mb (c1 :++: c2) bSource
Combines a binding inside another binding into a single binding.
mbSeparate :: 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 cc
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
Special-purpose functions for lifting primitives out of bindings
mbLiftChar :: Mb c Char -> CharSource
Lifts a Char
out of a multi-binding
mbLiftInteger :: Mb c Integer -> IntegerSource
Lifts an Integer
out of a multi-binding