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]
- deriveTypeElim :: Name -> Q [Dec]
- deriveTypeElimNamed :: String -> Name -> Q [Dec]

# Eliminator generation

## Term-level eliminators

`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:

- 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`

.

## Type-level eliminators

`deriveTypeElim`

and `deriveTypeElimNamed`

are like `deriveElim`

and
`deriveElimNamed`

except that they create *type*-level eliminators instead of
term-level ones. Here is an example showing how one might use
`deriveTypeElim`

:

```
data MyList a = MyNil | MyCons a (MyList a)
$(
````deriveTypeElim`

''MyList)

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

type ElimMyList :: forall (a ::`Type`

). forall (p :: MyList a`~>`

`Type`

) (l :: MyList a) ->`Apply`

p MyNil -> (forall (x :: a) (xs :: MyList a) ->`Apply`

p xs`~>`

`Apply`

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

p l type family ElimMyList p l pMyNil pMyCons where forall (a ::`Type`

) (p :: MyList a ~>`Type`

) (pMyNil ::`Apply`

p MyNil) (pMyCons :: forall (x :: a) (xs :: MyList a) ->`Apply`

p xs`~>`

`Apply`

p (MyCons x xs)). ElimMyList`a p MyNil pMyNil pMyCons = pMyNil forall (a ::`

a p (MyCons x' xs') pMyNil pMyCons =`Type`

) (p :: MyList a ~>`Type`

) (_pMyNil ::`Apply`

p MyNil) (pMyCons :: forall (x :: a) (xs :: MyList a) ->`Apply`

p xs`~>`

`Apply`

p (MyCons x xs)) x' xs'. ElimMyList`Apply`

(pMyCons x' xs') (ElimMyList @a p xs' pMyNil pMyCons)

Note the following differences from a term-level eliminator that `deriveElim`

would generate:

- Type-level eliminators do not use
`Sing`

. Instead, they use visible dependent quantification. That is, instead of generating`forall (x :: a). Sing x -> ...`

(as a term-level eliminator would do), a type-level eliminator would use`forall (x :: a) -> ...`

. - Term-level eliminators quantify
`p`

with an invisible`forall`

, whereas type-level eliminators quantify`p`

with a visible`forall`

. (Really,`p`

ought to be quantified visibly in both forms of eliminator, but GHC does not yet support visible dependent quantification at the term level.) - Type-level eliminators use (
`~>`

) in certain places where (`->`

) would appear in term-level eliminators. For instance, note the use of

in`Apply`

p xs`~>`

`Apply`

p (MyCons x xs)`ElimMyList`

above. This is done to make it easier to use type-level eliminators with defunctionalization symbols (which aren't necessary for term-level eliminators).

This comes with a notable drawback: type-level eliminators cannot support
data constructors where recursive occurrences of the data type appear in a
position other than the last field of a constructor. In other words,
`deriveTypeElim`

works on the `MyList`

example above, but not this variant:

data SnocList a = SnocNil | SnocCons (SnocList a) a

This is because `$(`

would generate an eliminator
with the following kind:`deriveTypeElim`

''SnocList)

type ElimSnocList :: forall (a ::`Type`

). forall (p :: SnocList a`~>`

`Type`

) (l :: SnocList a) ->`Apply`

p SnocNil -> (forall (xs :: SnocList a) ->`Apply`

p xs`~>`

(forall (x :: a) ->`Apply`

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

p l

Unfortunately, the kind

is
impredicative.`Apply`

p xs `~>`

(forall (x :: a) -> `Apply`

p (SnocCons x xs))

In addition to the language extensions that

`deriveElim`

requires, you'll need to enable these extensions in order to use`deriveTypeElim`

:StandaloneKindSignatures

UndecidableInstances

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

generates a type-level eliminator for the
datatype `deriveTypeElim`

dataName`dataName`

. The eliminator will follow these naming conventions:

- 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.

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

generates a type-level eliminator
named `deriveTypeElimNamed`

funName dataName`funName`

for the datatype `dataName`

.