[Haskell-cafe] A Specification for GADTs in Haskell?

Xuanrui Qi xuanrui at nagoya-u.jp
Tue Nov 26 14:54:16 UTC 2019

Hello all,

I recently came a cross a comment by Richard Eisenberg that there's
actually no specification for GADTs and creating one would be a major
research project (in a GHC proposal somewhere, I recall, but I don't
remember exactly where).

I was wondering what exactly does Richard's comment mean. What
constitutes a specification for GADTs in Haskell? I suppose typing
rules and semantics are necessary; what are the major roadblocks
hindering the creation of a formal specification for GADTs in Haskell?



Xuanrui Qi
Graduate School of Mathematics, Nagoya University

More information about the Haskell-Cafe mailing list