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 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:
- 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
.
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)). ElimMyLista 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'. ElimMyListApply
(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 generatingforall (x :: a). Sing x -> ...
(as a term-level eliminator would do), a type-level eliminator would useforall (x :: a) -> ...
. - Term-level eliminators quantify
p
with an invisibleforall
, whereas type-level eliminators quantifyp
with a visibleforall
. (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
inApply
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 usederiveTypeElim
:StandaloneKindSignatures
UndecidableInstances
deriveTypeElim :: Name -> Q [Dec] Source #
generates a type-level eliminator for the
datatype deriveTypeElim
dataNamedataName
. 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 dataNamefunName
for the datatype dataName
.