<br><br>On Saturday, May 7, 2016, Gershom B <<a href="mailto:gershomb@gmail.com">gershomb@gmail.com</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On May 7, 2016 at 10:30:05 PM, wren romano (<a href="javascript:;" onclick="_e(event, 'cvml', 'wren@community.haskell.org')">wren@community.haskell.org</a>) wrote:<br>
> Hi all,<br>
><br>
> There's been some discussion about whether to consider including GADTs<br>
> in the new report, but it's been mixed up with other stuff in the<br>
> thread on incorporating extensions wholesale, which has unfortunately<br>
> preempted/preceded the discussion about how to go about having such<br>
> discussions(!).<br>
><br>
> My position on the debate is that we should avoid having the debate,<br>
> just yet. (Which I intended but failed to get across in the email<br>
> which unintentionally started this all off.) I think we have many much<br>
> lower-hanging fruit and it'd be a better use of our time to try and<br>
> get those squared away first. Doing so will help us figure out and<br>
> debug the process for having such debates, which should help the GADT<br>
> debate itself actually be fruitful. As well as making progress on<br>
> other fronts, so we don't get mired down first thing.<br>
<br>
Thanks for this summary Wren. Let me add something I would be interested in seeing happen in the “meantime” — 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). A compliant compiler could then be required to have inference “at least” that good, but also be allowed to go “above and beyond”. Thus fully portable H2020 code might require more specified signatures than we need in GHC proper, but all such code would also typecheck in GHC. It seems to me that the creation of such an algorithm might be an interesting bit of research in itself.<br>
<br>
—Gershom</blockquote><div><br></div>I agree, there's definitely value in some research / engineering work that articulates a clear simple checker and a simple and slightly conservative inference alg , and that could pave a nice path towards gadts inclusion or at least a concrete starting point. Thanks for articulating this, I've been thinking much the same thing.  Of course the proof is in the pudding for how it works out :)<span></span><div><br></div><div><br></div><div>Peripherally, this also brings up the notion of type equality, and I'm a bit fuzzy about how big a chasm there is between what that means in Haskell 2010 vs more bleeding edge styles, or am I pointing at a shadows?<br><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 href="javascript:;" onclick="_e(event, 'cvml', 'Haskell-prime@haskell.org')">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>