Copyright | (c) Galois Inc 2013-2019 |
---|---|

Maintainer | Joe Hendrix <jhendrix@galois.com> |

Safe Haskell | None |

Language | Haskell98 |

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`

n`T`

.

`AnyType`

means that the type parameter in that position can be instantiated as any type

means that the type parameter in that position is the`DataArg`

n`n`

-th type parameter of the GADT being traversed (`T`

in the example)`TypeApp`

is type application`ConType`

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`

]