<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Hi Xuanrui,<div class=""><br class=""></div><div class="">Glad you're interested in pursuing this topic!</div><div class=""><br class=""></div><div class="">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).</div><div class=""><br class=""></div><div class="">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:</div><div class=""><br class=""></div><div class="">* GHC's type system and inference algorithm are well documented in <a href="https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/jfp-outsidein.pdf" class="">https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/jfp-outsidein.pdf</a> 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.</div><div class=""><br class=""></div><div class="">* These two papers describe type inference with GADTs: <a href="https://dl.acm.org/citation.cfm?id=2837665" class="">https://dl.acm.org/citation.cfm?id=2837665</a> and <a href="https://dl.acm.org/citation.cfm?id=3290322" class="">https://dl.acm.org/citation.cfm?id=3290322</a>. Neither is applicable to Haskell out-of-the-box.</div><div class=""><br class=""></div><div class="">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.</div><div class=""><br class=""></div><div class="">I hope this is helpful -- happy to expand on this if you like!</div><div class=""><br class=""></div><div class="">Richard<br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Nov 26, 2019, at 2:54 PM, Xuanrui Qi <<a href="mailto:xuanrui@nagoya-u.jp" class="">xuanrui@nagoya-u.jp</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class="">Hello all,<br class=""><br class="">I recently came a cross a comment by Richard Eisenberg that there's<br class="">actually no specification for GADTs and creating one would be a major<br class="">research project (in a GHC proposal somewhere, I recall, but I don't<br class="">remember exactly where).<br class=""><br class="">I was wondering what exactly does Richard's comment mean. What<br class="">constitutes a specification for GADTs in Haskell? I suppose typing<br class="">rules and semantics are necessary; what are the major roadblocks<br class="">hindering the creation of a formal specification for GADTs in Haskell?<br class=""><br class="">Thanks!<br class=""><br class="">Xuanrui<br class=""><br class="">-- <br class="">Xuanrui Qi<br class="">Graduate School of Mathematics, Nagoya University<br class=""><a href="https://www.xuanruiqi.com" class="">https://www.xuanruiqi.com</a><br class=""><br class="">_______________________________________________<br class="">Haskell-Cafe mailing list<br class="">To (un)subscribe, modify options or view archives go to:<br class="">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe<br class="">Only members subscribed via the mailman list are allowed to post.</div></div></blockquote></div><br class=""></div></body></html>