Re: Scope of committee (can we do *new* things?)
On May 8, 2016 at 9:25:33 PM, Richard Eisenberg (e...@cis.upenn.edu) wrote: > > I do absolutely think we should be cautious about addressing unimplemented > behavior. > I would be strongly against a new type-system extension that hasn't been > field-tested. > However, I do think pondering lexical/parsical changes (such as limber > separators) > should be considered in scope. While such changes should definitely be in scope, I do think that the proper mechanism would be to garner enough interest to get a patch into GHC (whether through discussion on the -prime list or elsewhere) and have an experimental implementation, even for syntax changes, before such proposals are considered ready for acceptance into a standard as such. But I also agree that discussion of things which may be in the pre-implementation phase are in scope — just that the next step is to get them past that phase before they’re considered for inclusion as such. There are enough traps in parsing that specification without an implementation is always a risky choice. Recall for example the case of fixity resolution, finally fixed in Haskell2010 (https://prime.haskell.org/wiki/FixityResolution) where the behavior in the report was at variance with all implementations. I would hope that if a segment of the prime committee wants to test-run an experimental syntax feature, then this would take sufficient precedence over concerns regarding “language fragmentation” that the GHC team would be open to guarding it behind a flag. Given the number of GHC developers involved in this effort, I think that’s not a bad estimation :-) Cheers, Gershom ___ Haskell-prime mailing list Haskell-prime@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
Scope of committee (can we do *new* things?)
On May 8, 2016, at 6:27 AM, Alexander Berntsen wrote: > > I realise now that the report is not the place to fix problems with > Haskell, but to standardise solutions that a high enough percentage of > packages already rely on. I misjudged the ambition level of the > report. Thus I withdraw this proposal to not waste the committees time > any further. The above snippet has been taken from the "Limber separators" thread. I don't wish to debate limber separators at the moment, but I think Alexander raises a good question here: Should we endeavor to take on any as-yet-unimplemented behavior that might make Haskell better? My own opinion is a resounding "yes!" If we say "no", we're left with a terrible chicken-and-egg problem. I have seen some proposed extensions to GHC be thrown out because they would fragment the language unnecessarily. Chief in my head is that proposal to allow `case`, `if`, `do`, etc., in a function application without parentheses or a $ operator. That is, to permit `runST do blah; blah`. (See https://ghc.haskell.org/trac/ghc/ticket/10843) A common rebuttal against this proposal was that implementing the extension would involve a lot of huffing and puffing over a few characters, and that now all Haskell readers may have to be aware of this new extension, even if an individual doesn't write with it. However, the Haskell Prime committee is a great place to debate such a change. If we move quickly, we can even implement it, get it into GHC (or some other Haskell compiler, I suppose), and get feedback before we set the standard in stone. I do absolutely think we should be cautious about addressing unimplemented behavior. I would be strongly against a new type-system extension that hasn't been field-tested. However, I do think pondering lexical/parsical changes (such as limber separators) should be considered in scope. Richard ___ Haskell-prime mailing list Haskell-prime@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
Re: The GADT debate
On Sun, May 8, 2016 at 1:38 AM, Carter Schonwald 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 Haskell-prime@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
Re: The GADT debate
On Sun, May 8, 2016 at 11:25 AM, 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. 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 Haskell-prime@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
Re: The GADT debate
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 > > ___ Haskell-prime mailing list Haskell-prime@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
Re: The GADT debate
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
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
Re: Limber separators
-BEGIN PGP SIGNED MESSAGE- Hash: SHA512 On 08/05/16 05:03, wren romano wrote: > One of my big concerns here is that the proposal is vague, and > therefore impossible to judge. It is intentionally somewhat vague because I would the committee to address this problem which is largely solved in many other languages, but remains a -- to many bizarre -- problem in Haskell > As an example of what I mean, what counts as a "separator"? Is it > a special case only commas? Why not also include the vertical pipe > in data type definitions? If you read my email, you will see that I *am* including them. > Coq and other ML-like languages allow a vertical pipe between the > "=" and the first constructor name, so why shouldn't we? Or, what > about when people do parser combinator stuff and use the (<|>) > operator as a "separator", should we handle that too? That's function (operator) application. I would think that it was entirely obvious that I did not mean that users should be able to write 'f f f f f f f x x x x x x x x' and have the compiler work out that the user meant 'f x'. If it wasn't, then I'm saying it now. I did not mean to include operators or function application. I'm not sure how that could even make sense. I am slightly bemused by the amount of complexity this list is imposing on a -- to me -- relatively straightforward idea. I realise now that the report is not the place to fix problems with Haskell, but to standardise solutions that a high enough percentage of packages already rely on. I misjudged the ambition level of the report. Thus I withdraw this proposal to not waste the committees time any further. Please note that I don't mean this email to be a critique of the scope or ambition of the report -- I think that standardising solutions should be the clearly most important goal of this committee. - -- Alexander alexan...@plaimi.net https://secure.plaimi.net/~alexander -BEGIN PGP SIGNATURE- Version: GnuPG v2 iQIcBAEBCgAGBQJXLxR6AAoJENQqWdRUGk8BtlYP/RBm8cMLm3HzJA6fPnRHhhbj tomHfLqgg/2ZDs05wHY4v0rI5KMmQzfsZIJAJbv8FiWUprkW3X6YaKetxyICIfh/ KmBsqppACDEi62OEB28QAgvRmKy5zrsJOiT2a8Dg2IHUqfHvfAtk11sC1kscWXNa cjtfn0etNvOfLEJLU1pjUXf5iTLrkR0JQSAUsGn3vXhneWeMx2SkanH2H5PUXv1c hVIbUWXGC5M/VU9fp5O1xckHHboSPRJlSQbMx8srtN+3A65UdRZfCoH2HQ34+Tc3 j1kVKV9zF6X0GAogq3gdzqicCgMgfA46P7z3YdneTov78N8XfeD5CGJQrns+/iCF kube5pYhjHRws89rHJQjSsH/Jqz4+CPFbkyhyCs/ZorRrPlsFhz5Vtu5oeQN3nqZ PyntRUyQUpAYMJuwwGs8x1rxGScq/s+/6PvduznnYKwJFtaz0WQStLUK9zNQFwxN xXcQ6pFkeFqXM1ideHpCpP0bg25LQZps4WkAk7sGEgl1SkTQkS+a1m0DDZbE85HN P2Jz+XORwd+Y+n7KBmZbxPQDgmH8z/6d23F1UPEBwTG3A3GFSVw+Devwf1eZrv1G p+SNbVQVQlLvMF4gfQmfkYUSBk8muOtJPcXvAXOeuLTsI/WfI2jHhndizT4tYFsm mavFWSy2Fg89K1d+w4c9 =3/+J -END PGP SIGNATURE- ___ Haskell-prime mailing list Haskell-prime@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
