- 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
- mkNuElimData :: Q Type -> Q [Dec]
- class NuElimList args where
- class NuElim1 f where
- data NuElimProof a
Applies a function in a multi-binding to an argument in a multi-binding that binds the same number and types of names.
Take a multi-binding inside another multi-binding and move the outer binding inside the inner one.
nuWithElimMulti args f takes a sequence
zero or more multi-bindings, each of type
Mb ctx ai for the same
ctx of bound names, and a function
f and does the
- Creates a multi-binding that binds names
n1,...,nn, one name for each type in
- Substitutes the names
n1,...,nnfor the names bound by each argument in the
argssequence, yielding the bodies of the
args(using the new name
n); and then
- Passes the sequence
n1,...,nnalong with the result of substituting into
argsto the function
f, which then returns the value for the newly created binding.
Note that the types in
args must each have a
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')
nuMultiWithElim but binds only one name.
nuMultiWithElim but takes only one argument
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
nuWithElim1. The structure of this class is
mostly hidden from the user; see
mkNuElimData to see how to create
instances of the
|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)|
Template Haskell function for creating NuElim instances for (G)ADTs.
Typical usage is to include the following line in the source file for
T (here assumed to have two type arguments):
$(mkNuElimData [t| forall a b . T a b |])
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
forall a for you.