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 SepDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Sun 23 Sep
Displayed time zone: Guadalajara, Mexico City, Monterrey change
10:20 - 12:00
GHCHIW at Illinois Central
Chair(s): Ben Gamari Well-Typed LLP
Simon Peyton Jones Microsoft, UKFile Attached
Matthew Pickering University of BristolMedia Attached
|Generalized Abstract GHC.Generics|
Ryan Scott Indiana University at Bloomington, USAFile Attached
|Lightning talk: CodeWorld: Teaching Haskell and mathematics to children|
Chris Smith Google, USA
|Lightning talk: CoreSpec: Verifying GHC with hs-to-coq|
|Lightning talk: The trick which makes exceptions-0.10.0 possible|
Samuel Gélineau SimSpaceMedia Attached