Copyright | (C) 2017 Ryan Scott |
---|---|

License | BSD-style (see the file LICENSE) |

Maintainer | Ryan Scott |

Stability | Experimental |

Portability | GHC |

Safe Haskell | Unsafe |

Language | Haskell2010 |

Generate dependently typed elimination functions using Template Haskell.

## Synopsis

- deriveElim :: Name -> Q [Dec]
- deriveElimNamed :: String -> Name -> Q [Dec]

# Eliminator generation

`deriveElim`

and `deriveElimNamed`

provide a way to automate the creation of
eliminator functions, which are mostly boilerplate. Here is a complete example
showing how one might use `deriveElim`

:

$(`singletons`

[d| data MyList a = MyNil | MyCons a (MyList a) |]) $(`deriveElim`

''MyList)

This will produce an eliminator function that looks roughly like the following:

elimMyList :: forall (a ::`Type`

) (p :: MyList a`~>`

`Type`

) (l :: MyList a).`Sing`

l ->`Apply`

p MyNil -> (forall (x :: a).`Sing`

x -> forall (xs :: MyList a).`Sing`

xs ->`Apply`

p xs ->`Apply`

p (MyCons x xs)) ->`Apply`

p l elimMyList SMyNil pMyNil _ = pMyNil elimMyList (SMyCons (x' ::`Sing`

x) (xs' ::`Sing`

xs)) pMyNil pMyCons = pMyCons x' xs' (elimMyList @a @p @xs pMyNil pMyCons)

There are some important things to note here:

- Because these eliminators use
`Sing`

under the hood, in order for`deriveElim`

to work, the`Sing`

instance for the data type given as an argument must be in scope. Moreover,`deriveElim`

assumes the naming conventions for singled constructors used by the`singletons`

library. (This is why the`singletons`

function is used in the example above). There is a convention for the order in which the arguments appear. The quantified type variables appear in this order:

The function arguments appear in this order:

- First, a
`Sing`

argument (

, in the above example).`Sing`

l - Next, there are arguments that correspond to each constructor. More on this in a second.

The return type is the predicate type variable applied to the data type
(

, the above example).`Apply`

p (MyCons x xs)

The type of each constructor argument also follows certain conventions:

- For each field, there will be a rank-2 type variable whose kind matches
the type of the field, followed by a matching
`Sing`

type. For instance, in the above example,`forall (x :: a).`

corresponds to the first field of`Sing`

x`MyCons`

. - In addition, if the field is a recursive occurrence of the data type,
an additional argument will follow the
`Sing`

type. This is best explained using the above example. In the`MyCons`

constructor, the second field (of type`MyCons a`

) is a recursive occurrence of`MyCons`

, so that corresponds to the type`forall (xs :: MyList a).`

, where`Sing`

xs ->`Apply`

p xs

is only present due to the recursion.`Apply`

p xs - Finally, the return type will be the predicate type variable applied
to a saturated occurrence of the data constructor
(

, in the above example).`Apply`

p (MyCons x xs)

You'll need to enable lots of GHC extensions in order for the code generated by

`deriveElim`

to typecheck. You'll need at least the following:AllowAmbiguousTypes

DataKinds

GADTs

PolyKinds

RankNTypes

ScopedTypeVariables

TemplateHaskell

TypeApplications

`deriveElim`

doesn't support every possible data type at the moment. It is known not to work for the following:- Data types defined using
`GADTs`

or`ExistentialQuantification`

- Data family instances
- Data types which use polymorphic recursion
(e.g.,
`data Foo a = Foo (Foo a)`

)

- Data types defined using

deriveElim :: Name -> Q [Dec] Source #

generates a top-level elimination function for the
datatype `deriveElim`

dataName`dataName`

. The eliminator will follow these naming conventions:
The naming conventions are:

- If the datatype has an alphanumeric name, its eliminator will have that name
with
`elim`

prepended. - If the datatype has a symbolic name, its eliminator will have that name
with
`~>`

prepended.

deriveElimNamed :: String -> Name -> Q [Dec] Source #

generates a top-level elimination
function named `deriveElimNamed`

funName dataName`funName`

for the datatype `dataName`

.