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.
- 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
- nuElimProof :: NuElimProof a
- mkNuElimData :: Q Type -> Q [Dec]
- class NuElimList args where
- nuElimListProof :: MapC NuElimProof args
- data NuElimProof a
Documentation
nuWithElimMulti :: NuElimList args => 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 => MapC (Mb (Nil :> a)) args -> (Name a -> MapC Identity args -> b) -> Binding a bSource
Similar to nuWithElimMulti
but binds only one name.
nuWithElim1 :: NuElim arg => Binding a arg -> (Name a -> arg -> b) -> Binding a bSource
Similar to 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
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.
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 NuElimProof argsSource
NuElimList Nil | |
(NuElimList args, NuElim a) => NuElimList (:> args a) |
data NuElimProof a Source