|
|
|
|
|
This page sketches the ideas how to equip `GHC.Generics` with type-level reasoning facilities.
|
|
|
|
|
|
|
|
|
Motivation
|
|
|
# Motivation
|
|
|
|
|
|
|
|
|
the gdiff library requires a family GADT for describing the constructors of datatypes that one wants to `diff` and `patch`. This family has to cover (identify) all appearing data type constructors in _value tree_ transitively. Given two such constructor identifiers gdiff uses propositional equality (called `decEq` in the library) to get hold of the constructor's data in a type-safe manner.
|
... | ... | @@ -16,8 +15,7 @@ Marriage of GHC.Generics with `gdiff` appears straightforward weren't there one |
|
|
|
|
|
To support this propositional equality in GHC.Generics we have to equip the {datatype, constructor and selector} metatypes with type-level information so that we can use Data.TypeEquality-provided functions (e.g. sameNat, sameSymbol) on them.
|
|
|
|
|
|
|
|
|
Metadata in `GHC.Generics`
|
|
|
# Metadata in `GHC.Generics`
|
|
|
|
|
|
- for data types: `D1 meta f p`
|
|
|
- for data constructors: `C1 meta f p` (potentially more than one per data type)
|
... | ... | @@ -27,4 +25,31 @@ Metadata in `GHC.Generics` |
|
|
Here `meta` is a private (phantom) type constructor which parametrises the `Datatype`, `Constructor` and `Selector` instances. The corresponding class constraint's methods give (runtime access) to the metainformation.
|
|
|
|
|
|
|
|
|
Implementation Idea |
|
|
An example session with GHCi is provided below to illustrate the current system:
|
|
|
|
|
|
```wiki
|
|
|
```
|
|
|
|
|
|
# Implementation Idea
|
|
|
|
|
|
|
|
|
In order to [TypeLevelReasoning](type-level-reasoning) to work data types must be indexed by some type-level decoration (e.g. `GHC.TypeLits`' `Nat` and `Symbol` kinds).
|
|
|
|
|
|
|
|
|
The idea is to change typecheck/TcGenGenerics to create
|
|
|
\`meta = Constr "Mod" "Bool" "True"
|
|
|
|
|
|
|
|
|
This idea is (partly) implemented on branch `wip/propeq-generics`. Here is a GHCi dialogue:
|
|
|
|
|
|
```wiki
|
|
|
Prelude> :m +GHC.Generics
|
|
|
Prelude GHC.Generics> :kind! Rep Bool ()
|
|
|
Rep Bool () :: *
|
|
|
= M1
|
|
|
D
|
|
|
(Dat "GHC.Generics" "Bool")
|
|
|
(M1 C (Constr (Dat "GHC.Generics" "Bool") "False") U1
|
|
|
:+: M1 C (Constr (Dat "GHC.Generics" "Bool") "True") U1)
|
|
|
()
|
|
|
``` |
|
|
\ No newline at end of file |