[Haskell-cafe] A Specification for GADTs in Haskell?
vamchale at gmail.com
Tue Nov 26 15:46:15 UTC 2019
A spec would be something in the spirit of the Haskell2010 perhaps? Typing rules written up, plus the syntax, plus specification for pattern matching.
> On Nov 26, 2019, at 8:54 AM, Xuanrui Qi <xuanrui at nagoya-u.jp> wrote:
> 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
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> Only members subscribed via the mailman list are allowed to post.
More information about the Haskell-Cafe