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)
- class Liftable a where
- class Liftable1 f where
- class Liftable2 f where
- mbList :: Mb c [a] -> [Mb c a]
- 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
type classes for lifting data out of bindings
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
The class Liftable1 f
gives a lifting function for each type f a
when a
itself is Liftable
.
The class Liftable2 f
gives a lifting function for each type f a b
when a
and b
are Liftable
.