Re: [ghc-steering-committee] Please review "Visible 'forall' in types of terms" #281

Back to the main point, it seems to be fairly consensual, right now, that #281 doesn't seem to have found the sweet spot which would make it work quite right. Not yet. I basically agree with the points raised so far. As I said earlier in the thread, I'm sympathetic with the goals, but unconvinced by the details. Is there a committee member which disagrees with the emerging consensus? On Tue, Nov 24, 2020 at 1:15 PM Simon Peyton Jones via ghc-steering-committee wrote:

* Having two name-spaces appears to be The Major Obstacle towards making satisfying incremental progress in the direction of dependent types.

* So perhaps we should have an extension -XSingleNameSpace that has a single name space, with all the consequences that would entail (like changing the syntax of tuple and list types).

* Then further extensions toward dependent types could require -XSingleNameSpace. If you don't want that, you don't get the new goodies. There would be no expectation that a dependent-types extension should fit well with the double-name-space situation; maybe the combination is actually disallowed.

* Or maybe the combination is allowed, but a bit clunky. For example, suppose a library defines f :: forall a -> blah Then, in a module with classic-Haskell name spaces, you'd have to say f (type Int) and not (f Int), forcibly setting the namespace.

It'd be good to have this conversation on GitHub, and perhaps #378 is the place to do that?

Simon

| -----Original Message----- | From: ghc-steering-committee < ghc-steering-committee-bounces@haskell.org> On | Behalf Of Joachim Breitner | Sent: 23 November 2020 08:10 | To: ghc-steering-committee@haskell.org | Subject: Re: [ghc-steering-committee] Please review "Visible 'forall' in | types of terms" #281 | | Hi, | | Richard roughly says what is my sentiment too… I’d phrase it like this: | | It seems that #281 would be rather straight forward, if it were not for the | fact that this is the first (of many?) extensions that allow types and terms | to occur in the same syntactic spot. So far, when mentally parsing a | program, I know where to look for types, and where to look for terms. #281 | breaks that, and has to come up with lots of subtle rules, that make me | uneasy. | | But that's not really #281’s fault – assuming we want to head towards | Dependent Haskell with a unified namespace, it’s a problem that needs to be | solved! But better have that discussion with a focus on that problem, and | have a plan that works in general. Maybe #270 is the right place to have | that discussion. | | My impression is that all (most?) of | those working towards a Dependent Haskell world assume that we get a unified | namespace with no punning, and all complexity (`type` sigils, `type`- | qualified imports) is around compatibility with modules that use punning, | with the hope that this is rare. Few are proposing to stick to a world of | two namespaces and punning and make _that_ ergonomic. Is that impression | correct? | | Do local modules (#283) alleviate the punning problem a bit? Given `data T = | T`, could we make it so that T is the type and T.T the constructor? | | But this really isn't the right place to throw out shower ideas. I wonder if | it would help if someone could maintain a wiki page with an overview of all | the numerous proposals and ideas thrown around to tackle the problem about | how we get from a world of two name spaces and punning to one with one | namespaces and no punning. | | | As for #281, unless I misjudge the urgency of that change, I’d be in favor | to park it until we have a good, generally applicable plan for mixing terms | and types. | | Cheers, | Joachim | | | | | Am Montag, den 23.11.2020, 03:35 +0000 schrieb Richard Eisenberg: | > My silence on this proposal is because I want to accept, but I agree with | Iavor that it's become too baroque. My #378 is, in part, an attempt to | clarify our stance on these sorts of features so that we can take a stab at | simplifying #281 by making it less expressive. | > | > So, I guess my vote is to delay decision on this proposal until we have | one for #378 (or #270, which can also help shed light on this one). | > | > Responding directly to Alejandro's concerns here: I actually don't really | understand. I think (1) is decided by | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com | %2Fghc-proposals%2Fghc-proposals%2Fblob%2Fmaster%2Fproposals%2F0081-forall- | arrow.rst&data=04%7C01%7Csimonpj%40microsoft.com %7Ccba94a6d611e470021260 | 8d88f87414e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C637417159812849940% | 7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwi | LCJXVCI6Mn0%3D%7C3000&sdata=vU3lOmJ6kFNfEuy9MOo6ZoapadyzGIXPZblhR9QYvD0% | 3D&reserved=0; we use this syntax in standalone kind signatures in GHC | 8.10. We *could* change this if there were a compelling reason, but this | proposal is just continuing an existing feature. By (2), I think you're | referring to all the complications in the proposals at how to deal with | names and syntax in arguments -- I wouldn't myself describe this as | conflating the two namespaces, but rather as defining a subtle set of rules | for interpreting ambiguous names. It's the subtlety of these rules that | makes me uncomfortable. For (3), I don't really think there's much there -- | and what there is seems to require (2) (and vice versa). Do you have an | example of a type-inference interaction you're worried about here? | > | > Richard | > | > > On Nov 22, 2020, at 12:09 PM, Alejandro Serrano Mena < trupill@gmail.com> | wrote: | > > | > > Hi all, | > > For me, there are two main concerns here: | > > This could be split on different proposals: (1) using the “forall a | > > ->” syntax, (2) conflating the type and term syntax and namespaces, (3) | introducing checking and inference for it; I find the claim that you can | just take the Quick Look Impredicativity paper, make a couple of | adjustments, and get correct checking and inference. This kind of big change | is the one for which I would actually expect a peer-reviewed paper. | > > | > > Regards, | > > Alejandro | > > | > > El El sáb, 21 nov 2020 a las 10:10, Joachim Breitner escribió: | > > > Dear Committee, | > > > | > > > Iavor suggested to reject this proposal, but we have not heard a | > > > lot here yet. Especially before rejecting proposals, we probably | > > > owe a careful analysis, possibly with suggestions of ways forward | > > > (splitting the proposal into smaller pieces maybe? Iavor says | > > > there are many changes there). | > > > | > > > If we have continued silence, we’d reject. | > > > | > > > Cheers, | > > > Joachim | > > > | > > > | > > > Am Mittwoch, den 11.11.2020, 13:41 -0800 schrieb Iavor Diatchki: | > > > > Hello, | > > > > | > > > > Proposal #281 has been submitted for review by the committee again, | please read through it and let's have a discussion. Here are links to the | proposal's discussion section, and the proposal text: | > > > > | > > > > https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F% | > > > > 2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F281&da | > > > > ta=04%7C01%7Csimonpj%40microsoft.com %7Ccba94a6d611e4700212608d88 | > > > > f87414e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C63741715981 | > > > > 2849940%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2lu | > > > > MzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=oWBR%2BJue6s | > > > > 2bh7WU7lRhfHTcaDrQoUHzveh7e4XqWJE%3D&reserved=0 | > > > > https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F% | > > > > 2Fgithub.com%2Fint-index%2Fghc-proposals%2Fblob%2Fvisible-forall | > > > > %2Fproposals%2F0000-visible-forall.rst&data=04%7C01%7Csimonp | > > > > j%40microsoft.com %7Ccba94a6d611e4700212608d88f87414e%7C72f988bf8 | > > > > 6f141af91ab2d7cd011db47%7C1%7C1%7C637417159812849940%7CUnknown%7 | > > > > CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWw | > > > > iLCJXVCI6Mn0%3D%7C3000&sdata=cfbyhbDYnPX%2BC7BKrak3mzPEFyiXY | > > > > wPhza3T1sv2X2I%3D&reserved=0 | > > > > | > > > > While I suggested acceptance on the previous version, I am leaning | towards rejecting the proposal now. My reasoning is that I hadn't fully | understood all the aspects of the original proposal, and the new proposal | seems to lack a simple modular specification. There are *many* changes | described in the document, but I found it hard to understand what is the | current design, from the point of view of a user of the feature, as opposed | to someone trying to implement it. | > > > > | > > > > I'd be curious about what others think. | > > > > | > > > > -Iavor | > > > > | > > > > | > > > > _______________________________________________ | > > > > ghc-steering-committee mailing list | > > > > ghc-steering-committee@haskell.org | > > > > https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F% | > > > > 2Fmail.haskell.org %2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering | > > > > -committee&data=04%7C01%7Csimonpj%40microsoft.com %7Ccba94a6d | > > > > 611e4700212608d88f87414e%7C72f988bf86f141af91ab2d7cd011db47%7C1% | > > > > 7C1%7C637417159812849940%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjA | > > > > wMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&s | > > > > data=JJjZfHZhOTQ6yo31ucKEFHC9hNIXG9McT18FbuYbgvI%3D&reserved | > > > > =0 | > > > -- | > > > Joachim Breitner | > > > mail@joachim-breitner.de | > > > | > > > https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fw | > > > ww.joachim-breitner.de %2F&data=04%7C01%7Csimonpj%40microsoft.c | > > > om%7Ccba94a6d611e4700212608d88f87414e%7C72f988bf86f141af91ab2d7cd0 | > > > 11db47%7C1%7C1%7C637417159812849940%7CUnknown%7CTWFpbGZsb3d8eyJWIj | > > > oiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C300 | > > > 0&sdata=BArEbQSBvN4zsTDWtN9PW3klvk1c05lX8hhm2jMKk5E%3D&res | > > > erved=0 | > > > | > > > | > > > _______________________________________________ | > > > ghc-steering-committee mailing list | > > > ghc-steering-committee@haskell.org | > > > https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2F | > > > mail.haskell.org %2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering-com | > > > mittee&data=04%7C01%7Csimonpj%40microsoft.com %7Ccba94a6d611e47 | > > > 00212608d88f87414e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C63 | > > > 7417159812849940%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQI | > > > joiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=JJjZfHZ | > > > hOTQ6yo31ucKEFHC9hNIXG9McT18FbuYbgvI%3D&reserved=0 | > > | > > _______________________________________________ | > > ghc-steering-committee mailing list | > > ghc-steering-committee@haskell.org | > > https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fma | > > il.haskell.org %2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering-committ | > > ee&data=04%7C01%7Csimonpj%40microsoft.com %7Ccba94a6d611e47002126 | > > 08d88f87414e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C6374171598 | > > 12849940%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzI | > > iLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=JJjZfHZhOTQ6yo31ucK | > > EFHC9hNIXG9McT18FbuYbgvI%3D&reserved=0 | > | > _______________________________________________ | > ghc-steering-committee mailing list | > ghc-steering-committee@haskell.org | > https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail | > .haskell.org %2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering-committee&a | > mp;data=04%7C01%7Csimonpj%40microsoft.com %7Ccba94a6d611e4700212608d88f | > 87414e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C637417159812859933 | > %7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6I | > k1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=er3qe80%2BcqnIn3UIKfjuGu4VDwkH7 | > jEosJqR45eKvn4%3D&reserved=0 | -- | Joachim Breitner | mail@joachim-breitner.de | | https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joachim | - | breitner.de%2F&data=04%7C01%7Csimonpj%40microsoft.com %7Ccba94a6d611e4700 | 212608d88f87414e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C63741715981285 | 9933%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1 | haWwiLCJXVCI6Mn0%3D%7C3000&sdata=dyYFsh09gm4vxafb%2FRfa36jb8QT%2BBlHUtx1 | OK6AMf%2BE%3D&reserved=0 | | | _______________________________________________ | ghc-steering-committee mailing list | ghc-steering-committee@haskell.org | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail.haske | ll.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering- | committee&data=04%7C01%7Csimonpj%40microsoft.com %7Ccba94a6d611e470021260 | 8d88f87414e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C637417159812859933% | 7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwi | LCJXVCI6Mn0%3D%7C3000&sdata=er3qe80%2BcqnIn3UIKfjuGu4VDwkH7jEosJqR45eKvn | 4%3D&reserved=0 _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee