Re: [ghc-steering-committee] Proposal #281: Visible "forall" in terms; rec: accept

Yes, the proposal does argue explicitly against '@', I just don't find the argument all that convincing. In my mind the use of '@' as a visibility specifier is the inconsistency, as '@' has been the symbol for type application both in Core and Haskell for much longer than it has been used as a visibility specifier. On Fri, Oct 29, 2021, at 11:01, Vladislav Zavialov (int-index) wrote:

The problem with ‘@‘, as explained by Richard, is cited right next to the Alternative 5.

However, I agree with Eric that the ’type’ herald feels excessive. It’s not something I personally intend to use. However, I remember Simon PJ and Iavor liked it (if I recall correctly), hence its inclusion in the proposal.

I don’t think it hurts either, though. We can accommodate different programming styles.

- Vlad

...

On 29 Oct 2021, at 17:53, Simon Peyton Jones via ghc-steering-committee wrote:

| 1. f @Int -- traditional, invisible forall 2. f Int -- visible forall, | Int is unambiguous 3. f (type Int) -- visible forall, Int is ambiguous

Perhaps it would help, in the proposal, to make explicit the argument *against* using @ as the herald for all type arguments. I remember that there *is* such an argument, and I found it quite convincing, but I can't remember it now. Maybe it is there somewhere?

Vlad/Richard?

Simon

PS: I am leaving Microsoft at the end of November 2021, at which point simonpj@microsoft.com will cease to work. Use simon.peytonjones@gmail.com instead. (For now, it just forwards to simonpj@microsoft.com.)

| -----Original Message----- | From: ghc-steering-committee On Behalf Of Eric Seidel | Sent: 29 October 2021 02:16 | To: ghc-steering-committee@haskell.org | Subject: Re: [ghc-steering-committee] Proposal #281: Visible "forall" | in terms; rec: accept | | I would still prefer alternative 5 (using @ as the type herald). I | really dislike that we would now have three ways to specify a type | argument: | | 1. f @Int -- traditional, invisible forall 2. f Int -- visible forall, | Int is unambiguous 3. f (type Int) -- visible forall, Int is ambiguous | | Ideally I would have single syntax for specifying type arguments, | which was historically (1). I know that many people would like to | unify the term and type syntaxes, so I'm ok with (2) as well even | though the T2T algorithm seemed quite involved. But adding (3) really | feels excessive. | | But I believe I'm a small minority in this opinion, so I don't want to | stand in the way of a very useful feature. | | On Wed, Oct 27, 2021, at 09:56, Richard Eisenberg wrote: | > It has been two weeks. I have heard no argument against this | proposal, | > but Simon Marlow (in the springtime) expressed some puzzlement. | Simon, | > what are you thinking about this now? With no further response, I | will | > accept this proposal on Friday. | > | > Others are also very welcome to chime in! | > | > Thanks, all! | > Richard | > | >> On Oct 27, 2021, at 5:30 AM, Spiwack, Arnaud | wrote: | >> | >> I think that the proposal makes a great job at listing the issues. | It's quite transparent about this, I'm not sure what I could add. | >> | >> On Wed, Oct 27, 2021 at 11:29 AM Simon Peyton Jones | wrote: | >>> I was indeed confused! Apologies. | >>> | >>> But my main point remains: enumerating a list of inconvenient side | effects and corner cases would be a great service. | >>> | >>> Simon | >>> | >>> PS: I am leaving Microsoft at the end of November 2021, at which | >>> point simonpj@microsoft.com will cease to work. Use | >>> simon.peytonjones@gmail.com instead. (For now, it just forwards | to | >>> simonpj@microsoft.com.) | >>> | >>> | -----Original Message----- | >>> | From: Vladislav Zavialov (int-index) | >>> | Sent: 27 October 2021 10:10 | >>> | To: Simon Peyton Jones | >>> | Cc: Spiwack, Arnaud ; Richard | Eisenberg | >>> | ; ghc-steering-committee >> | committee@haskell.org> | >>> | Subject: Re: [ghc-steering-committee] Proposal #281: Visible | "forall" | >>> | in terms; rec: accept | >>> | | >>> | Simon, perhaps you're thinking of another proposal that is | >>> | currently under committee's consideration? | >>> | | >>> | Arnaud was commenting on #281, and you seem to be talking about | #425. | >>> | | >>> | - Vlad | >>> | | >>> | > On 27 Oct 2021, at 12:05, Simon Peyton Jones via ghc- | steering- | >>> | committee wrote: | >>> | > | >>> | > There are a lot of inconvenient side effects and corner cases | >>> | > > Arnaud, could you enumerate them? Even if (as I strongly | >>> | hope) we accept this proposal, it's good to have a concrete | list | >>> | of things to | >>> | bear in mind. I for one do not have such list in my head. | >>> | > | >>> | > One principle that the proposal espouses (but perhaps does | not | >>> | call out explicitly) is that it should be possible to write an | explicit | >>> | binder for every in-scope variable. So instead of | >>> | > data T (a :: k -> k) = ... I want to write | >>> | > data T @k (a :: k -> k) = ... with an explicit | binder | >>> | > for k. | >>> | > | >>> | > So I see the proposal as removing an ad-hoc wart in the | language. | >>> | But I may be blind to the "inconvenient side effects and corner | cases" | >>> | and I'd welcome a list of such cases. | >>> | > | >>> | > Simon | >>> | > | >>> | > | >>> | > PS: I am leaving Microsoft at the end of November 2021, at | >>> | which point > simonpj@microsoft.com will cease to work. | >>> | > Usesimon.peytonjones@gmail.com instead. (For now, it just | >>> | forwards to > simonpj@microsoft.com.) > > From: | >>> | ghc-steering-committee > | >>> | On Behalf Of | Spiwack, | >>> | > Arnaud > Sent: 27 October 2021 09:20 > To: Richard Eisenberg | >>> | > Cc: ghc-steering-committee | >>> | | >>> | > Subject: Re: [ghc-steering-committee] Proposal #281: Visible | >>> | "forall" | >>> | > in terms; rec: accept | >>> | > | >>> | > I've been struggling to have an opinion on this PR. I'm very | >>> | sympathetic to the goal of the proposal (and this latest | rendition | >>> | of the proposal is a really good document). There are a lot of | >>> | inconvenient side effects and corner cases (but, to be fair, | these | >>> | are not special to this proposal: they are inherent to the | >>> | dependent types plan). But I'm fairly convinced that this is | the | >>> | best possible approach, or close enough. | >>> | > | >>> | > | >>> | > | >>> | > So yes, I don't really feel strongly about it. But on | balance, | >>> | I think that I'm in favour. | > | > _______________________________________________ | > 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%7C69ae5d5e09784d08370708d99a | > | 79ccff%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637710670242799539 | > | %7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6I | > | k1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=hGq4xMd5RsHOEGwF7lr3QCuMUXrxSwl | > cjEH89KLcy5A%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&data=04%7C01%7Csimonpj%40microsoft.com%7C69ae5d5e09784d0 | 8370708d99a79ccff%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C6377106 | 70242799539%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMz | IiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=hGq4xMd5RsHOEGwF7lr3 | QCuMUXrxSwlcjEH89KLcy5A%3D&reserved=0 _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee