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. Whenever the debate occurs, here's a summary of the relevant emails so that they are not lost, buried in the emails of time: * Andres Löh puts forth criteria on how to judge whether extensions should be included. Mentions GADTs as an example of something that, if we decide they're a good idea in principle (criterion #1), then we should work towards things which will help them be easier to feasibly/sensibly specify (criterion #2) https://mail.haskell.org/pipermail/haskell-prime/2016-May/004104.html * wren agrees with the criteria, loves GADTs, thinks they do not fully satisfy criterion #2 https://mail.haskell.org/pipermail/haskell-prime/2016-May/004115.html * Simon Peyton Jones says type inference for GADTs has, in fact, stabilized. Albeit, not entirely satisfactory because it's "a bit operational" https://mail.haskell.org/pipermail/haskell-prime/2016-May/004119.html * Henrik Nilsson thinks GADTs are one of the most important extensions to Haskell (fwiw, wren agrees). Also worries about being able to specify type inference declaratively. https://mail.haskell.org/pipermail/haskell-prime/2016-May/004120.html * Dominique Devriese suggests including MonoLocalBinds, finds "let should not be generalized" convincing https://mail.haskell.org/pipermail/haskell-prime/2016-May/004117.html * wren finds "let should not be generalized" unconvincing https://mail.haskell.org/pipermail/haskell-prime/2016-May/004145.html -- Live well, ~wren _______________________________________________ Haskell-prime mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime |
On May 7, 2016 at 10:30:05 PM, wren romano ([hidden email]) 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 _______________________________________________ Haskell-prime mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime |
On Saturday, May 7, 2016, Gershom B <[hidden email]> wrote: On May 7, 2016 at 10:30:05 PM, wren romano (<a href="javascript:;" onclick="_e(event, 'cvml', 'wren@community.haskell.org')">wren@...) wrote: 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 [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime |
In reply to this post by Gershom Bazerman
On May 7, 2016, at 11:05 PM, Gershom B <[hidden email]> 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 [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime |
On Sunday, May 8, 2016, Richard Eisenberg <[hidden email]> wrote:
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 [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime |
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 <[hidden email]> wrote:
_______________________________________________ Haskell-prime mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime |
In reply to this post by Richard Eisenberg-2
On Sun, May 8, 2016 at 11:25 AM, Richard Eisenberg <[hidden email]> wrote:
> On May 7, 2016, at 11:05 PM, Gershom B <[hidden email]> 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. If all three of those signatures are present, doesn't that make "inference" trivial? If I understand you correctly, the only thing to do here would be to check the types, right? I am curious though. Since we don't have true/anonymous type-level functions, why do we need the signatures on every branch (assuming the scrutinee and whole-expression types are given)? I can see why they'd be required in Coq/Agda/etc, but it's less clear why they'd be required in Haskell per se -- Live well, ~wren _______________________________________________ Haskell-prime mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime |
In reply to this post by Carter Schonwald
On Sun, May 8, 2016 at 1:38 AM, Carter Schonwald
<[hidden email]> wrote: > 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? Generally speaking, notions of "equality" are a major source of complication in any dependently typed theory. The issue isn't coming up with a story that works, but rather choosing between a number of different stories each of which works in slightly different ways. This problem of "equality" is the bulk of why I think it'd be good to postpone the GADT (and TypeFamily) debate. One Haskell-specific example of why defining equality is hard is when we try to handle both the "equalities" induced by dependent case-analysis as well as the "equalities" induced by newtype definitions. Though we use the same word for them, they're two entirely different notions of "equality". However, since they both exist, we must have some story for how these two notions interact with one another (including possibly "not at all"). The new role-typing stuff is one approach to handling this, but many people feel it's overly complicated or otherwise not quite the right way forward. If we add GADTs to the report, then we also need to define how to type check dependent case-analysis, which seems to require introducing type equality, which in turn requires specifying how the semantic notion of type equality interacts with the operational notion of representation equality introduced by newtypes, which is still imo an open area of research. If we can come up with some story that lets us make progress towards eventually including GADTs (and TypeFamilies) while avoiding the equality tarpit, I'm all for it. I'd just really rather avoid the tarpit until we have other easier things squared away. ... One possible way forward may be to introduce the syntax for (~) constraints and defining them merely as "delayed unification constraints". This would require including unification in the report, but may be doable in a way that allows non-unification-based implementations as well. The reason I bring this possibility up now is that it helps handle some other situations where we don't even have GADTs or TypeFamilies. In particular, when FlexibleInstances is enabled it allows for non-linear use of type variables in the instance head. However, this is often not what we mean since "instance Foo (Bar i i)" means that the two parameters to Bar must be unified *prior* to selecting that instance; which often leads to type inference issues since we can't resolve the instance eagerly enough. Whereas, often times what is actually desired is "instance (i ~ j) => Foo (Bar i j)" which causes us to select the instance immediately if the type constructor is Bar, and then *after* committing to the instance we then try to unify the two parameters. Thus, adding delayed unification constraints would be helpful for adding (something like) FlexibleInstances to the report. Of course, "delayed unification constraints" don't have any sort of evidence associated with them like the dependent case-analysis equalities do; so, again, we'd want to make sure to phrase things in such a way that we don't prematurely commit to more than we intend. -- Live well, ~wren _______________________________________________ Haskell-prime mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime |
In reply to this post by Richard Eisenberg-2
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:[hidden email]] On Behalf Of Richard Eisenberg Sent: 08 May 2016 16:25 To: Gershom B Cc: [hidden email] List Subject: Re: The GADT debate On May 7, 2016, at 11:05 PM, Gershom B <[hidden email]> 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 [hidden email] 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/financialmarkets/Pages/doddfrankdisclosures.aspx for important information with respect to derivative products. _______________________________________________ Haskell-prime mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime |
Free forum by Nabble | Edit this page |