GHC.Generics has seen enormous success as a tool for writing datatype-generic programs in Haskell. But its scope is currently limited, as the API that GHC.Generics exposes is only suitable for working plain old abstract datatypes. That is, one cannot write sensible Generic instances for GADTs.
In this talk, we propose an extension to GHC.Generics which would bridge this gap. Our technique relies on three observations:
- One can express any GADT in an equivalent form where all existential quantification is made explicit.
- Using various GHC language extensions, one can construct generic representation types that model existential quantification at the type level.
- Using the QuantifiedConstraints language extension, one can reason about existentially quantified types in class instances without needing to know what those types are ahead of time.
We will demonstrate this technique to generically derive instances for progressively more complex GADTs, and briefly discuss how our work could be simplified by future GHC extensions, such as dependent types.
|Slides: Generalized Abstract GHC.Generics (gagg-no-nums.pdf)||209KiB|
Sun 23 Sep Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change
10:20 - 12:00
Simon Peyton JonesMicrosoft, UKFile Attached
Matthew PickeringUniversity of BristolMedia Attached
|Generalized Abstract GHC.Generics|
Ryan ScottIndiana University at Bloomington, USAFile Attached
|Lightning talk: CodeWorld: Teaching Haskell and mathematics to children|
Chris SmithGoogle, USA
|Lightning talk: CoreSpec: Verifying GHC with hs-to-coq|
|Lightning talk: The trick which makes exceptions-0.10.0 possible|
Samuel GélineauSimSpaceMedia Attached