On Saturday, May 7, 2016, Gershom B <gersh...@gmail.com> wrote: > On May 7, 2016 at 10:30:05 PM, wren romano (w...@community.haskell.org > <javascript:;>) wrote: > > Hi all, > > > > There's been some discussion about whether to consider including GADTs > > in the new report, but it's been mixed up with other stuff in the > > thread on incorporating extensions wholesale, which has unfortunately > > preempted/preceded the discussion about how to go about having such > > discussions(!). > > > > My position on the debate is that we should avoid having the debate, > > just yet. (Which I intended but failed to get across in the email > > which unintentionally started this all off.) I think we have many much > > lower-hanging fruit and it'd be a better use of our time to try and > > get those squared away first. Doing so will help us figure out and > > debug the process for having such debates, which should help the GADT > > debate itself actually be fruitful. As well as making progress on > > other fronts, so we don't get mired down first thing. > > 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. > > —Gershom
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 :) 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? > _______________________________________________ > Haskell-prime mailing list > Haskell-prime@haskell.org <javascript:;> > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime >
_______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
