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 forderiveElim
to work, theSing
instance for the data type given as an argument must be in scope. Moreover,deriveElim
assumes the naming conventions for singled constructors used by thesingletons
library. (This is why thesingletons
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 ofSing
xMyCons
. - 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 theMyCons
constructor, the second field (of typeMyCons a
) is a recursive occurrence ofMyCons
, so that corresponds to the typeforall (xs :: MyList a).
, whereSing
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
orExistentialQuantification
- 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
dataNamedataName
. 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 dataNamefunName
for the datatype dataName
.