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.

Hi Xuanrui, Glad you're interested in pursuing this topic! By specification, I mean that it should be possible to write down a set of (simple... or simple-ish) rules describing A) what programs are accepted by the compiler, and B) what will happen when these programs are run. (A) is called either typing rules or static semantics; (B) is called operational or dynamic semantics (or sometimes just semantics). The problem with GADTs is that we don't have that set of rules, at least not for Haskell's realization of GADTs. There is some work on this area: * GHC's type system and inference algorithm are well documented in https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/jfp-outs... https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/jfp-outs... This paper lays out an overly-permissive set of rules for when GADTs should be accepted, but some programs are rejected that the rules suggest would be accepted. * These two papers describe type inference with GADTs: https://dl.acm.org/citation.cfm?id=2837665 https://dl.acm.org/citation.cfm?id=2837665 and https://dl.acm.org/citation.cfm?id=3290322 https://dl.acm.org/citation.cfm?id=3290322. Neither is applicable to Haskell out-of-the-box. While I'm grateful to anyone who braves my thesis, it does not really address this problem, focusing much more on the internal language than on type inference. I suppose you could extract something from Chapter 6 (on type inference), but there are key bits missing there -- notably, any specification of a solver. I hope this is helpful -- happy to expand on this if you like! Richard

On Nov 26, 2019, at 2:54 PM, 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.