parameterized-utils-2.1.1: Classes and data structures for working with data-kind indexed types

Copyright(c) Galois Inc 2013-2019
MaintainerJoe Hendrix <jhendrix@galois.com>
Safe HaskellNone
LanguageHaskell2010

Data.Parameterized.TH.GADT

Contents

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

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 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 Source #

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 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

polyEqF

Methods

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

polyEq :: u -> v -> Bool Source #

Instances
PolyEq (NatRepr m) (NatRepr n) Source # 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

PolyEq (BoolRepr m) (BoolRepr n) Source # 
Instance details

Defined in Data.Parameterized.BoolRepr

PolyEq (PeanoRepr m) (PeanoRepr n) Source # 
Instance details

Defined in Data.Parameterized.Peano

Template haskell utilities that may be useful in other contexts.

conPat 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.

data TypePat Source #

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] 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 [SigT (VarT a) StarT]. Note that there may be type *variables* not referenced in the returned array; this simply returns the type *arguments*.

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

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