| Copyright | (c) Galois Inc 2013-2019 |
|---|---|
| Maintainer | Joe Hendrix <jhendrix@galois.com> |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.Parameterized.TH.GADT
Description
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.
AnyTypemeans that the type parameter in that position can be instantiated as any typemeans that the type parameter in that position is theDataArgnn-th type parameter of the GADT being traversed (Tin the example)TypeAppis type applicationConTypespecifies 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.
Minimal complete definition
Template haskell utilities that may be useful in other contexts.
type DataD = DatatypeInfo Source #
lookupDataType' :: Name -> Q DatatypeInfo Source #
Arguments
| :: 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]