- nuWithElimMulti :: NuElimList args => MapC f ctx -> MapC (Mb ctx) args -> (MapC Name ctx -> MapC Identity args -> b) -> Mb ctx b
- nuWithElim :: NuElimList args => MapC (Mb (Nil :> a)) args -> (Name a -> MapC Identity args -> b) -> Binding a b
- nuWithElim1 :: NuElim arg => Binding a arg -> (Name a -> arg -> b) -> Binding a b
- class NuElim a where
- mkNuElimData :: Q Type -> Q [Dec]
- class NuElimList args where
- data NuElimProof a
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')
nuWithElimMulti but binds only one name.
nuWithElimMulti 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
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.