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

[Vanessa McHale]

A spec would be something in the spirit of the Haskell2010 perhaps? Typing rules written up, plus the syntax, plus specification for pattern matching.

Cheers,
Vanessa McHale

> 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?
> 
> Thanks!
> 
> Xuanrui
> 
> -- 
> Xuanrui Qi
> Graduate School of Mathematics, Nagoya University
> https://www.xuanruiqi.com
> 
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.