<div dir="ltr">Hello,<div><br></div><div>what is the state with the semantic specification of GADTs?  I am wondering if they fit in the usual CPO-style semantics for Haskell, or do we need some more exotic mathematical structure to give semantics to the language.</div><div><br></div><div>-Iavor</div><div><br></div><div><br></div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, May 8, 2016 at 8:36 AM, Carter Schonwald <span dir="ltr"><<a href="mailto:carter.schonwald@gmail.com" target="_blank">carter.schonwald@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class=""><br><br>On Sunday, May 8, 2016, Richard Eisenberg <<a href="mailto:eir@cis.upenn.edu" target="_blank">eir@cis.upenn.edu</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
On May 7, 2016, at 11:05 PM, Gershom B <<a>gershomb@gmail.com</a>> wrote:<br>
><br>
> an attempt (orthogonal to the prime committee at first) to specify an algorithm for inference that is easier to describe and implement than OutsideIn, and which is strictly less powerful. (And indeed whose specification can be given in a page or two of the report).<br>
<br>
Stephanie Weirich and I indeed considered doing such a thing, which conversation was inspired by my joining the Haskell Prime committee. We concluded that this would indeed be a research question that is, as yet, unanswered in the literature. The best we could come up with based on current knowledge would be to require type signatures on:<br>
<br>
1. The scrutinee<br>
2. Every case branch<br>
3. The case as a whole<br>
<br>
With all of these type signatures in place, GADT type inference is indeed straightforward. As a strawman, I would be open to standardizing GADTs with these requirements in place and the caveat that implementations are welcome to require fewer signatures. Even better would be to do this research and come up with a good answer. I may very well be open to doing such a research project, but not for at least a year. (My research agenda for the next year seems fairly solid at this point.) If someone else wants to spearhead and wants advice / a sounding board / a less active co-author, I may be willing to join.<br>
<br>
Richard</blockquote><div><br></div><div><br></div></span><div>This sounds awesome.  One question I'm wondering about is what parts of the type inference problem aren't part of the same challenge in equivalent dependent data types? I've been doing some Intersting stuff on the latter front recently. </div><div><br></div><div>It seems that those two are closely related, but I guess there might be some complications in Haskell semantics for thst? And or is this alluded to in existing work on gadts?<span></span></div><div class="HOEnZb"><div class="h5"><div><br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
_______________________________________________<br>
Haskell-prime mailing list<br>
<a>Haskell-prime@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime</a><br>
</blockquote>
</div></div><br>_______________________________________________<br>
Haskell-prime mailing list<br>
<a href="mailto:Haskell-prime@haskell.org">Haskell-prime@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime</a><br>
<br></blockquote></div><br></div>