Data.Parameterized.TH.GADT

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.

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 [(TypePat, ExpQ)]. Each 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 NatRepr n in a value of type T.

• AnyType means that the type parameter in that position can be instantiated as any type
• DataArg n means that the type parameter in that position is the 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

structuralEquality declares a structural equality predicate.

structuralTypeEquality :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ

structuralTypeEquality f returns a function with the type: forall x y . f x -> f y -> Maybe (x :~: y)

structuralTypeOrd

Arguments

:: TypeQ

-> [(TypePat, ExpQ)]

List of type patterns to match.

-> ExpQ

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

structuralTraversal tp generates a function that applies a traversal f to the subterms with free variables in tp.

structuralShowsPrec :: TypeQ -> ExpQ

structuralShow tp generates a function with the type tp -> ShowS that shows the constructor.

structuralHash :: TypeQ -> ExpQ

structuralHash tp generates a function with the type Int -> tp -> Int that hashes type.

class PolyEq u v where

A polymorphic equality operator that generalizes TestEquality.

Minimal complete definition

polyEqF

Methods

polyEqF :: u -> v -> Maybe (u :~: v)

polyEq :: u -> v -> Bool

Instances

PolyEq (NatRepr m) (NatRepr n)

Defined in Data.Parameterized.NatRepr.Internal

Methods

polyEqF :: NatRepr m -> NatRepr n -> Maybe (NatRepr m :~: NatRepr n)

polyEq :: NatRepr m -> NatRepr n -> Bool

PolyEq (BoolRepr m) (BoolRepr n)

Defined in Data.Parameterized.BoolRepr

Methods

polyEqF :: BoolRepr m -> BoolRepr n -> Maybe (BoolRepr m :~: BoolRepr n)

polyEq :: BoolRepr m -> BoolRepr n -> Bool

PolyEq (PeanoRepr m) (PeanoRepr n)

Defined in Data.Parameterized.Peano

Methods

polyEqF :: PeanoRepr m -> PeanoRepr n -> Maybe (PeanoRepr m :~: PeanoRepr n)

polyEq :: PeanoRepr m -> PeanoRepr n -> Bool

TestEquality f => PolyEq (Assignment f x) (Assignment f y)

Defined in Data.Parameterized.Context.Safe

Methods

polyEqF :: Assignment f x -> Assignment f y -> Maybe (Assignment f x :~: Assignment f y)

polyEq :: Assignment f x -> Assignment f y -> Bool

Template haskell utilities that may be useful in other contexts.

type DataD = DatatypeInfo

lookupDataType' :: Name -> Q DatatypeInfo

asTypeCon :: Monad m => String -> Type -> m Name

conPat

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.

data TypePat

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)

Constructors

TypeApp TypePat TypePat

The application of a type.

AnyType

Match any type.

DataArg Int

Match the i'th argument of the data type we are traversing.

ConType TypeQ

Match a ground type.

dataParamTypes :: DatatypeInfo -> [Type]

assocTypePats :: [Type] -> [(TypePat, v)] -> Type -> Q (Maybe v)

Find value associated with first pattern that matches given pat if any.