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

[Richard Eisenberg]

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20191126/5dbc5f73/attachment.html>