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

Copyright | (c) Galois Inc 2013-2019
Maintainer | Joe Hendrix <jhendrix@galois.com>
Safe Haskell | None
Language | Haskell2010

Data.Parameterized.TH.GADT

Contents

- Instance generators
- Repr generators ("singletons")
- Template haskell utilities that may be useful in other contexts.

Description

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
  - polyEqF :: u -> v -> Maybe (u :~: v)
  - polyEq :: u -> v -> Bool
- mkRepr :: Name -> DecsQ
- mkKnownReprs :: Name -> DecsQ
- type DataD = DatatypeInfo
- lookupDataType' :: Name -> Q DatatypeInfo
- asTypeCon :: String -> Type -> Q Name
- conPat :: ConstructorInfo -> String -> Q (Pat, [Name])
- data TypePat
  - = TypeApp TypePat TypePat
  - | AnyType
  - | DataArg Int
  - | ConType TypeQ
- 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 `[(`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

Instances details

PolyEq (BoolRepr m) (BoolRepr n) Source # |
Instance details Defined in Data.Parameterized.BoolRepr Methods polyEqF :: BoolRepr m -> BoolRepr n -> Maybe (BoolRepr m :~: BoolRepr n) Source # polyEq :: BoolRepr m -> BoolRepr n -> Bool Source #
PolyEq (NatRepr m) (NatRepr n) Source # |
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods polyEqF :: NatRepr m -> NatRepr n -> Maybe (NatRepr m :~: NatRepr n) Source # polyEq :: NatRepr m -> NatRepr n -> Bool Source #
PolyEq (PeanoRepr m) (PeanoRepr n) Source # |
Instance details Defined in Data.Parameterized.Peano Methods polyEqF :: PeanoRepr m -> PeanoRepr n -> Maybe (PeanoRepr m :~: PeanoRepr n) Source # polyEq :: PeanoRepr m -> PeanoRepr n -> Bool Source #

# Repr generators ("singletons")

When working with data kinds with run-time representatives, we encourage users of `parameterized-utils` to use the following convention. Given a data kind defined by

    data T = ...

users should also supply a GADT `TRepr` parameterized by `T`, e.g.

    data TRepr (t :: T) where ...

Each constructor of `TRepr` should correspond to a constructor of `T`. If `T` is defined by

    data T = A | B Nat

we have a corresponding

    data TRepr (t :: T) where
      ARepr :: TRepr 'A
      BRepr :: NatRepr w -> TRepr ('B w)

Assuming the user of `parameterized-utils` follows this convention, we provide the Template Haskell construct `mkRepr` to automate the creation of the `TRepr` GADT. We also provide `mkKnownReprs`, which generates `KnownRepr` instances for that GADT type. See the documentation for those two functions for more detailed explanations.

NB: These macros are inspired by the corresponding macros provided by `singletons-th`, and the "repr" programming idiom is very similar to the one used by `singletons`.

mkRepr :: Name -> DecsQ Source #

Generate a "repr" or singleton type from a data kind. For nullary constructors, this works as follows:

    data T1 = A | B | C
    $(mkRepr ''T1)
    ======>
    data T1Repr (tp :: T1)
      where
        ARepr :: T1Repr 'A
        BRepr :: T1Repr 'B
        CRepr :: T1Repr 'C

For constructors with fields, we assume each field type `T` already has a corresponding repr type `TRepr :: T -> *`.

    data T2 = T2_1 T1 | T2_2 T1
    $(mkRepr ''T2)
    ======>
    data T2Repr (tp :: T2)
      where
        T2_1Repr :: T1Repr tp -> T2Repr ('T2_1 tp)
        T2_2Repr :: T1Repr tp -> T2Repr ('T2_2 tp)

Constructors with multiple fields work fine as well:

    data T3 = T3 T1 T2
    $(mkRepr ''T3)
    ======>
    data T3Repr (tp :: T3)
      where
        T3Repr :: T1Repr tp1 -> T2Repr tp2 -> T3Repr ('T3 tp1 tp2)

This is generally compatible with other "repr" types provided by `parameterized-utils`, such as `NatRepr` and `PeanoRepr`:

    data T4 = T4_1 Nat | T4_2 Peano
    $(mkRepr ''T4)
    ======>
    data T4Repr (tp :: T4)
      where
        T4Repr :: NatRepr tp1 -> PeanoRepr tp2 -> T4Repr ('T4 tp1 tp2)

The data kind must be "simple", i.e. it must be monomorphic and only contain user-defined data constructors (no lists, tuples, etc.). For example, the following will not work:

    data T5 a = T5 a
    $(mkRepr ''T5)
    ======>
    Foo.hs:1:1: error:
        Exception when trying to run compile-time code:
          mkRepr cannot be used on polymorphic data kinds.

Similarly, this will not work:

    data T5 = T5 [Nat]
    $(mkRepr ''T5)
    ======>
    Foo.hs:1:1: error:
        Exception when trying to run compile-time code:
          mkRepr cannot be used on this data kind.

Note that at a minimum, you will need the following extensions to use this macro:

    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE KindSignatures #-}
    {-# LANGUAGE TemplateHaskell #-}

mkKnownReprs :: Name -> DecsQ Source #

Generate `KnownRepr` instances for each constructor of a data kind. Given a data kind `T`, we assume a repr type `TRepr (t :: T)` is in scope with structure that perfectly matches `T` (using `mkRepr` to generate the repr type will guarantee this).

Given data kinds `T1`, `T2`, and `T3` from the documentation of `mkRepr`, and the associated repr types `T1Repr`, `T2Repr`, and `T3Repr`, we can use `mkKnownReprs` to generate these instances like so:

    $(mkKnownReprs ''T1)
    ======>
    instance KnownRepr T1Repr 'A where
      knownRepr = ARepr
    instance KnownRepr T1Repr 'B where
      knownRepr = BRepr
    instance KnownRepr T1Repr 'C where
      knownRepr = CRepr

    $(mkKnownReprs ''T2)
    ======>
    instance KnownRepr T1Repr tp =>
             KnownRepr T2Repr ('T2_1 tp) where
      knownRepr = T2_1Repr knownRepr

    $(mkKnownReprs ''T3)
    ======>
    instance (KnownRepr T1Repr tp1, KnownRepr T2Repr tp2) =>
             KnownRepr T3Repr ('T3_1 tp1 tp2) where
      knownRepr = T3_1Repr knownRepr knownRepr

The same restrictions that apply to `mkRepr` also apply to `mkKnownReprs`. The data kind must be "simple", i.e. it must be monomorphic and only contain user-defined data constructors (no lists, tuples, etc.).

Note that at a minimum, you will need the following extensions to use this macro:

    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE KindSignatures #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE TemplateHaskell #-}

Also, `mkKnownReprs` must be used in the same module as the definition of the repr type (not necessarily for the data kind).

# Template haskell utilities that may be useful in other contexts.

type DataD = DatatypeInfo Source #

lookupDataType' :: Name -> Q DatatypeInfo Source #

asTypeCon :: String -> Type -> Q Name Source #

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.