Copyright | (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner |
---|---|
License | BSD3 |
Maintainer | emw4@rice.edu |
Stability | experimental |
Portability | GHC |
Safe Haskell | None |
Language | Haskell98 |
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
- nuMulti :: HList f ctx -> (HList Name ctx -> b) -> Mb ctx b
- nus :: HList f ctx -> (HList Name ctx -> b) -> Mb ctx b
- emptyMb :: a -> Mb Nil a
- cmpName :: Name a -> Name b -> Maybe (a :~: b)
- mbNameBoundP :: Mb ctx (Name a) -> Either (Member ctx a) (Name a)
- mbCmpName :: Mb c (Name a) -> Mb c (Name b) -> Maybe (a :~: b)
- elimEmptyMb :: Mb Nil a -> a
- mbCombine :: Mb c1 (Mb c2 b) -> Mb (c1 :++: c2) b
- mbSeparate :: HList any ctx2 -> Mb (ctx1 :++: ctx2) a -> Mb ctx1 (Mb ctx2 a)
- mbToProxy :: Mb ctx a -> HList Proxy ctx
- mbSwap :: Mb ctx1 (Mb ctx2 a) -> Mb ctx2 (Mb ctx1 a)
- mbApply :: Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
- nuMultiWithElim :: TypeCtx ctx => (HList Name ctx -> HList Identity args -> b) -> HList (Mb ctx) args -> Mb ctx b
- nuWithElim :: (Name a -> HList Identity args -> b) -> HList (Mb (Nil :> a)) args -> Binding a b
- nuMultiWithElim1 :: TypeCtx ctx => (HList Name ctx -> arg -> b) -> Mb ctx arg -> Mb ctx b
- nuWithElim1 :: (Name a -> arg -> b) -> Binding a arg -> Binding a b
Abstract types
A Name a
is a bound name that is associated with type a
.
An Mb ctx b
is a multi-binding that binds one name for each type
in ctx
, where ctx
has the form
.
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 Nil
:>
t1 :>
... :>
tnMbTypeRepr
for the body type, to ensure
that the names given in the pair can be relaced by fresher names.
NuMatching a => NuMatching (Mb ctx a) Source |
Multi-binding constructors
nu :: (Name a -> b) -> Binding a b Source
nu f
creates a binding which binds a fresh name n
and whose
body is the result of f n
.
nuMulti :: HList f ctx -> (HList Name ctx -> b) -> Mb ctx b Source
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 HList
f ctxctx
at the
term level; thus it is unimportant what the type function f
is.
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
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
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.
Operations on multi-bindings
elimEmptyMb :: Mb Nil a -> a Source
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 Source
Combines a binding inside another binding into a single binding.
mbSeparate :: HList any ctx2 -> Mb (ctx1 :++: ctx2) a -> Mb ctx1 (Mb ctx2 a) Source
Separates a binding into two nested bindings. The first argument, of
type
, is a "phantom" argument to indicate how
the context HList
any c2c
should be split.
mbToProxy :: Mb ctx a -> HList Proxy ctx Source
Returns a proxy object that enumerates all the types in ctx.
mbSwap :: Mb ctx1 (Mb ctx2 a) -> Mb ctx2 (Mb ctx1 a) Source
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 Source
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 => (HList Name ctx -> HList Identity args -> b) -> HList (Mb ctx) args -> Mb ctx b Source
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 inctx
; - Substitutes the names
n1,...,nn
for the names bound by each argument in theargs
sequence, yielding the bodies of theargs
(using the new namen
); and then - Passes the sequence
n1,...,nn
along with the result of substituting intoargs
to the functionf
, 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 ('Nil' :> f :> a) (\_ ('Nil' :> 'Identity' f' :> 'Identity' a') -> f' a')
nuWithElim :: (Name a -> HList Identity args -> b) -> HList (Mb (Nil :> a)) args -> Binding a b Source
Similar to nuMultiWithElim
but binds only one name.
nuMultiWithElim1 :: TypeCtx ctx => (HList Name ctx -> arg -> b) -> Mb ctx arg -> Mb ctx b Source
Similar to nuMultiWithElim
but takes only one argument
nuWithElim1 :: (Name a -> arg -> b) -> Binding a arg -> Binding a b Source
Similar to nuMultiWithElim
but takes only one argument that binds
a single name.