wiki:GenericsPropositionalEquality

This page sketches the ideas how to equip GHC.Generics with type-level reasoning facilities. This page describes work in progress. Initially responsible for this page is Gabor Greif.

Status Nov 2014

At the HacBerin 2014 GGR and JPM discussed the issue and we settled it in a way so that no changes to GHC are necessary. The trick is to obtain type equality witness from the Rep T and push that down to its innards. This way we need no propeq for constructors etc. Also Pedro is working towards a clean solution utilizing DataKinds.

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

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.

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)
  • for selectors: S1 meta f p (potentially more than one per constructor)

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.

An example session with GHCi is provided below to illustrate the current system:

Prelude> :m +GHC.Generics 
Prelude GHC.Generics> :kind! Rep Bool ()
Rep Bool () :: *
= M1
    D
    GHC.Generics.D1Bool
    (M1 C GHC.Generics.C1_0Bool U1 :+: M1 C GHC.Generics.C1_1Bool U1)
    ()

Implementation Idea

In order to TypeLevelReasoning 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" instead of meta = GHC.Generics.C1_1Bool

This idea is (partly) implemented on branch wip/generics-propeq. Here is a GHCi dialogue:

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

Given this metainformation reflected at the type level, propositional equality can be implemented by resorting to KnownSymbol and sameSymbol from GHC.TypeLits.

There is a small problem, though: We get orphan instance warnings because Dat and Constr do not carry the original datatype as an index.

An Aside: why Datatype?

Consider this current constraint on data types:

class Datatype d where
  datatypeName :: t d f a -> [Char]
  moduleName :: t d f a -> [Char]
  ...

Given the fact that for d = (Dat "GHC.Generics" "Bool") both pieces of information can be reified from the type-level, why do we need this constraint at all?

The Conservative Approach

After observing that Datatype is essentially just KnownSymbol × KnownSymbol we can ask the question:

Can we distill a type-level equality witness from Datatype constraints?

Unsurprisingly the answer is "yes". GHC.Generics could provide a function

sameDatatype :: (Datatype l, Datatype r) => Proxy l -> Proxy r -> Maybe (l :~: r)

and implement it in the same unsafe fashion as GHC.TypeLits does for sameSymbol.

This should be sufficient to satisfy gdiff's requirements on propositional equality.

The only con that I see with this approach is that module GHC.Generics gets additional dependencies on import Data.Proxy, import Unsafe.Coerce and import Data.Type.Equality.

For Constructor and Selector we would need to add further base class constraints:

class Datatype c => Constructor c where
  ...

class Constructor s => Selector s where
  ...

GHC would need to also instantiate these base constraints for constructors and selectors.

Update: I have implemented this in part, and it works. Unfortunately it can be used to subvert the type system, by comparing two different constructors with sameDatatype and obtain type equality for the constructors as long as they are from the same ADT. I am working on an improved scheme to fix this.

Last modified 3 years ago Last modified on Dec 19, 2014 7:41:00 PM