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

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 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.