On Saturday, May 7, 2016, Gershom B wrote:

On May 7, 2016 at 10:30:05 PM, wren romano (wren@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

On May 7, 2016, at 11:05 PM, Gershom B wrote:

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).

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: 1. The scrutinee 2. Every case branch 3. The case as a whole 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. Richard

Hello, 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. -Iavor On Sun, May 8, 2016 at 8:36 AM, Carter Schonwald

wrote:

On Sunday, May 8, 2016, Richard Eisenberg wrote:

...

On May 7, 2016, at 11:05 PM, Gershom B wrote:

...

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).

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:

1. The scrutinee 2. Every case branch 3. The case as a whole

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.

Richard

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.

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?

...

_______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org 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

Do you really need that many type signatures? I remember trying to work out what extra information is needed when type checking case with dependent types. If memory serves, you can get by with just specifying the single (type) function that is instantiated in each arm and in the conclusion. Maybe something similar is possible here. -----Original Message----- From: Haskell-prime [mailto:haskell-prime-bounces@haskell.org] On Behalf Of Richard Eisenberg Sent: 08 May 2016 16:25 To: Gershom B Cc: haskell-prime@haskell.org List Subject: Re: The GADT debate On May 7, 2016, at 11:05 PM, Gershom B wrote:

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).

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: 1. The scrutinee 2. Every case branch 3. The case as a whole 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. Richard _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime This email and any attachments are confidential and may also be privileged. If you are not the intended recipient, please delete all copies and notify the sender immediately. You may wish to refer to the incorporation details of Standard Chartered PLC, Standard Chartered Bank and their subsidiaries at http://www.standardchartered.com/en/incorporation-details.html Insofar as this communication contains any market commentary, the market commentary has been prepared by sales and/or trading desk of Standard Chartered Bank or its affiliate. It is not and does not constitute research material, independent research, recommendation or financial advice. Any market commentary is for information purpose only and shall not be relied for any other purpose, and is subject to the relevant disclaimers available at http://wholesalebanking.standardchartered.com/en/utility/Pages/d-mkt.aspx Insofar as this e-mail contains the term sheet for a proposed transaction, by responding affirmatively to this e-mail, you agree that you have understood the terms and conditions in the attached term sheet and evaluated the merits and risks of the transaction. We may at times also request you to sign on the term sheet to acknowledge in respect of the same. Please visit http://wholesalebanking.standardchartered.com/en/capabilities/financialmarke... for important information with respect to derivative products.