Data.Binding.Hobbits.NuElim

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.

Documentation

nuWithElimMulti :: NuElimList args => MapC f ctx -> MapC (Mb ctx) args -> (MapC Name ctx -> MapC Identity args -> b) -> Mb ctx b

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 in ctx;
• Substitutes the names n1,...,nn for the names bound by each argument in the args sequence, yielding the bodies of the args (using the new name n); and then
• Passes the sequence n1,...,nn along with the result of substituting into args to the function f, 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 b

Similar to nuWithElimMulti but binds only one name.

nuWithElim1 :: NuElim arg => Binding a arg -> (Name a -> arg -> b) -> Binding a b

Similar to nuWithElimMulti but takes only one argument that binds a single name.

class NuElim a where

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.

Methods

nuElimProof :: NuElimProof a

Instances

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)

NuElim a => NuElim (Mb ctx a)

mkNuElimData :: Q Type -> Q [Dec]

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 NuElim (T a b). It is also possible to include a context in the forall type; for example, if we define the 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 where

Methods

nuElimListProof :: MapC NuElimProof args

Instances

NuElimList Nil

(NuElimList args, NuElim a) => NuElimList (:> args a)

data NuElimProof a