Safe Haskell | None |
---|
This module defines the NuElim typeclass, which allows eliminations
of (multi-) bindings. The high-level idea is that, when a fresh name
is created with nu
, the fresh name can also be substituted for the
bound name in a binding. See the documentation for nuWithElim1
and
nuWithElimMulti
for details.
- mbApply :: (NuElim a, NuElim b) => Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
- mbMapAndSwap :: NuElim a => (Mb ctx1 a -> b) -> Mb ctx1 (Mb ctx2 a) -> Mb ctx2 b
- mbRearrange :: NuElim a => Mb ctx1 (Mb ctx2 a) -> Mb ctx2 (Mb ctx1 a)
- nuMultiWithElim :: (NuElimList args, NuElim b) => MapC f ctx -> MapC (Mb ctx) args -> (MapC Name ctx -> MapC Identity args -> b) -> Mb ctx b
- nuWithElim :: (NuElimList args, NuElim b) => MapC (Mb (Nil :> a)) args -> (Name a -> MapC Identity args -> b) -> Binding a b
- nuMultiWithElim1 :: (NuElim arg, NuElim b) => MapC f ctx -> Mb ctx arg -> (MapC Name ctx -> arg -> b) -> Mb ctx b
- nuWithElim1 :: (NuElim arg, NuElim b) => Binding a arg -> (Name a -> arg -> b) -> Binding a b
- class NuElim a where
- nuElimProof :: NuElimProof a
- mkNuElimData :: Q Type -> Q [Dec]
- class NuElimList args where
- nuElimListProof :: MapC NuElimObj args
- class NuElim1 f where
- nuElimProof1 :: NuElim a => NuElimObj (f a)
- data NuElimProof a
Documentation
mbApply :: (NuElim a, NuElim b) => Mb ctx (a -> b) -> Mb ctx a -> Mb ctx bSource
Applies a function in a multi-binding to an argument in a multi-binding that binds the same number and types of names.
mbRearrange :: NuElim a => 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 inner one.
NOTE: This is not yet implemented.
nuMultiWithElim :: (NuElimList args, NuElim b) => MapC f ctx -> MapC (Mb ctx) args -> (MapC Name ctx -> MapC Identity args -> b) -> Mb ctx bSource
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 NuElim
instance;
this is represented with the NuElimList
type class.
Here are some examples:
commuteFun :: (NuElim a, NuElim b) => Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b commuteFun f a = nuWithElimMulti ('mbToProxy' f) ('Nil' :> f :> a) (\_ ('Nil' :> 'Identity' f' :> 'Identity' a') -> f' a')
nuWithElim :: (NuElimList args, NuElim b) => MapC (Mb (Nil :> a)) args -> (Name a -> MapC Identity args -> b) -> Binding a bSource
Similar to nuMultiWithElim
but binds only one name.
nuMultiWithElim1 :: (NuElim arg, NuElim b) => MapC f ctx -> Mb ctx arg -> (MapC Name ctx -> arg -> b) -> Mb ctx bSource
Similar to nuMultiWithElim
but takes only one argument
nuWithElim1 :: (NuElim arg, NuElim b) => Binding a arg -> (Name a -> arg -> b) -> Binding a bSource
Similar to nuMultiWithElim
but takes only one argument that binds
a single name.
Instances of the NuElim a
class allow the type a
to be used with
nuWithElimMulti
and nuWithElim1
. The structure of this class is
mostly hidden from the user; see mkNuElimData
to see how to create
instances of the NuElim
class.
NuElim Char | |
NuElim Int | |
NuElim a => NuElim [a] | |
NuElim (Name a) | |
(NuElim a, NuElim b) => NuElim (a -> b) | |
(NuElim a, NuElim b) => NuElim (Either a b) | |
(NuElim a, NuElim b) => NuElim (a, b) | |
(NuElim1 f, NuElimList ctx) => NuElim (MapC f ctx) | |
NuElim a => NuElim (Mb ctx a) | |
(NuElim a, NuElim b, NuElim c) => NuElim (a, b, c) | |
(NuElim a, NuElim b, NuElim c, NuElim d) => NuElim (a, b, c, d) |
mkNuElimData :: Q Type -> Q [Dec]Source
Template Haskell function for creating NuElim instances for (G)ADTs.
Typical usage is to include the following line in the source file for
(G)ADT T
(here assumed to have two type arguments):
$(mkNuElimData [t| forall a b . T a b |])
The mkNuElimData
call here will create an instance declaration for
. It is also possible to include a context in the
forall type; for example, if we define the NuElim
(T a b)ID
data type as follows:
data ID a = ID a
then we can create a NuElim
instance for it like this:
$( mkNuElimData [t| NuElim a => ID a |])
Note that, when a context is included, the Haskell parser will add
the forall a
for you.
class NuElimList args whereSource
nuElimListProof :: MapC NuElimObj argsSource
NuElimList Nil | |
(NuElimList args, NuElim a) => NuElimList (:> args a) |
nuElimProof1 :: NuElim a => NuElimObj (f a)Source
data NuElimProof a Source