[Haskell-cafe] A Specification for GADTs in Haskell?
xuanrui at nagoya-u.jp
Tue Nov 26 14:54:16 UTC 2019
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?
Graduate School of Mathematics, Nagoya University
More information about the Haskell-Cafe