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 | |||
10:20 25mTalk | GHC Update HIW Simon Peyton Jones Microsoft, UK File Attached | ||
10:45 25mTalk | Source Plugins HIW Matthew Pickering University of Bristol Media Attached | ||
11:10 25mTalk | Generalized Abstract GHC.Generics HIW Ryan Scott Indiana University at Bloomington, USA File Attached | ||
11:35 8mTalk | Lightning talk: CodeWorld: Teaching Haskell and mathematics to children HIW Chris Smith Google, USA | ||
11:43 8mTalk | Lightning talk: CoreSpec: Verifying GHC with hs-to-coq HIW File Attached | ||
11:51 9mTalk | Lightning talk: The trick which makes exceptions-0.10.0 possible HIW Samuel Gélineau SimSpace Media Attached |