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-outsidein.pdf  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 and 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 <xuanrui@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.