Copyright | (c) Galois Inc 2013-2019 |
---|---|
Maintainer | Joe Hendrix <jhendrix@galois.com> |
Safe Haskell | None |
Language | Haskell2010 |
Description : Template Haskell primitives for working with large GADTs
This module declares template Haskell primitives so that it is easier to work with GADTs that have many constructors.
Synopsis
- structuralEquality :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ
- structuralTypeEquality :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ
- structuralTypeOrd :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ
- structuralTraversal :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ
- structuralShowsPrec :: TypeQ -> ExpQ
- structuralHash :: TypeQ -> ExpQ
- structuralHashWithSalt :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ
- class PolyEq u v where
- type DataD = DatatypeInfo
- lookupDataType' :: Name -> Q DatatypeInfo
- asTypeCon :: String -> Type -> Q Name
- conPat :: ConstructorInfo -> String -> Q (Pat, [Name])
- data TypePat
- dataParamTypes :: DatatypeInfo -> [Type]
- assocTypePats :: [Type] -> [(TypePat, v)] -> Type -> Q (Maybe v)
Instance generators
The Template Haskell instance generators structuralEquality
,
structuralTypeEquality
, structuralTypeOrd
, and structuralTraversal
employ heuristics to generate valid instances in the majority of cases. Most
failures in the heuristics occur on sub-terms that are type indexed. To
handle cases where these functions fail to produce a valid instance, they
take a list of exceptions in the form of their second parameter, which has
type [(
. Each TypePat
, ExpQ
)]TypePat
is a matcher that tells the
TH generator to use the ExpQ
to process the matched sub-term. Consider the
following example:
data T a b where C1 :: NatRepr n -> T () n instance TestEquality (T a) where testEquality = $(structuralTypeEquality [t|T|] [ (ConType [t|NatRepr|] `TypeApp` AnyType, [|testEquality|]) ])
The exception list says that structuralTypeEquality
should use
testEquality
to compare any sub-terms of type
in a value of
type NatRepr
nT
.
AnyType
means that the type parameter in that position can be instantiated as any type
means that the type parameter in that position is theDataArg
nn
-th type parameter of the GADT being traversed (T
in the example)TypeApp
is type applicationConType
specifies a base type
The exception list could have equivalently (and more precisely) have been specified as:
[(ConType [t|NatRepr|] `TypeApp` DataArg 1, [|testEquality|])]
The use of DataArg
says that the type parameter of the NatRepr
must
be the same as the second type parameter of T
.
structuralEquality :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ Source #
structuralEquality
declares a structural equality predicate.
structuralTypeEquality :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ Source #
structuralTypeEquality f
returns a function with the type:
forall x y . f x -> f y -> Maybe (x :~: y)
structuralTypeOrd f
returns a function with the type:
forall x y . f x -> f y -> OrderingF x y
This implementation avoids matching on both the first and second parameters in a simple case expression in order to avoid stressing GHC's coverage checker. In the case that the first and second parameters have unique constructors, a simple numeric comparison is done to compute the result.
structuralTraversal :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ Source #
structuralTraversal tp
generates a function that applies
a traversal f
to the subterms with free variables in tp
.
structuralShowsPrec :: TypeQ -> ExpQ Source #
structuralShow tp
generates a function with the type
tp -> ShowS
that shows the constructor.
structuralHash :: TypeQ -> ExpQ Source #
Deprecated: Use structuralHashWithSalt
structuralHash tp
generates a function with the type
Int -> tp -> Int
that hashes type.
All arguments use hashable
, and structuralHashWithSalt
can be
used instead as it allows user-definable patterns to be used at
specific types.
structuralHashWithSalt :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ Source #
structuralHashWithSalt tp
generates a function with the type
Int -> tp -> Int
that hashes type.
The second arguments is for generating user-defined patterns to replace
hashWithSalt
for specific types.
class PolyEq u v where Source #
A polymorphic equality operator that generalizes TestEquality
.
Template haskell utilities that may be useful in other contexts.
type DataD = DatatypeInfo Source #
lookupDataType' :: Name -> Q DatatypeInfo Source #
:: ConstructorInfo | constructor information |
-> String | generated name prefix |
-> Q (Pat, [Name]) | pattern and bound names |
Given a constructor and string, this generates a pattern for matching the expression, and the names of variables bound by pattern in order they appear in constructor.
A type used to describe (and match) types appearing in generated pattern
matches inside of the TH generators in this module (structuralEquality
,
structuralTypeEquality
, structuralTypeOrd
, and structuralTraversal
)
dataParamTypes :: DatatypeInfo -> [Type] Source #
The dataParamTypes function returns the list of Type arguments
for the constructor. For example, if passed the DatatypeInfo for a
newtype Id a = MkId a
then this would return [
. Note that there may be type *variables* not referenced
in the returned array; this simply returns the type *arguments*.SigT
(VarT
a)
StarT
]