The GADT debate

[Carter Schonwald]

On Saturday, May 7, 2016, Gershom B <gershomb at gmail.com> wrote:

> On May 7, 2016 at 10:30:05 PM, wren romano (wren at 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 at haskell.org <javascript:;>
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-prime/attachments/20160508/60b3d5ca/attachment.html>