... | ... | @@ -4,7 +4,7 @@ This page sketches the ideas how to equip `GHC.Generics` with type-level reasoni |
|
|
# Motivation
|
|
|
|
|
|
|
|
|
the [ gdiff library](https://hackage.haskell.org/package/gdiff) 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` appeals to propositional equality (called `decEq` in the library) to get hold of the constructor's data in a type-safe manner.
|
|
|
the [ gdiff library](https://hackage.haskell.org/package/gdiff) 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 the *value tree* transitively. Given two such constructor identifiers `gdiff` appeals to propositional equality (called `decEq` in the library) to get hold of the constructor's data in a type-safe manner.
|
|
|
|
|
|
[GHC.Generics](http://www.haskell.org/ghc/docs/latest/html/libraries/base-4.7.0.0/GHC-Generics.html) provides a `Rep t p` (representation of the data structure at the type level) for every data type when the user demands `deriving Generic`. Metadata is attached to parts of this representation which can be queried for names, modules, fixity, etc. at runtime.
|
|
|
|
... | ... | @@ -12,7 +12,7 @@ the [ gdiff library](https://hackage.haskell.org/package/gdiff) requires a famil |
|
|
Marriage of `GHC.Generics` with `gdiff` appears straightforward weren't there one detail: the metadata is not available at the type level, so `gdiff`'s requirement for propositional equality cannot be satisfied.
|
|
|
|
|
|
|
|
|
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.Type.Equality`-provided functions (e.g. sameNat, sameSymbol) on them.
|
|
|
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.Type.Equality`-provided functions (e.g. `sameNat`, `sameSymbol`) on them.
|
|
|
|
|
|
# Metadata in `GHC.Generics`
|
|
|
|
... | ... | |