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

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 mailto:simonpj@microsoft.com> 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 mailto:simonpj@microsoft.com will cease to work. Use simon.peytonjones@gmail.com mailto:simon.peytonjones@gmail.com instead. (For now, it just forwards to simonpj@microsoft.com mailto:simonpj@microsoft.com.)

| -----Original Message----- | From: Vladislav Zavialov (int-index) mailto:vlad.z.4096@gmail.com> | Sent: 27 October 2021 10:10 | To: Simon Peyton Jones mailto:simonpj@microsoft.com> | Cc: Spiwack, Arnaud mailto:arnaud.spiwack@tweag.io>; Richard Eisenberg | mailto:rae@richarde.dev>; ghc-steering-committee mailto: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 mailto:ghc-steering-committee@haskell.org> 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 mailto:simonpj@microsoft.com will cease to work. | > Usesimon.peytonjones@gmail.com mailto:Usesimon.peytonjones@gmail.com instead. (For now, it just forwards | to | > simonpj@microsoft.com mailto:simonpj@microsoft.com.) | > | > From: ghc-steering-committee | > mailto:ghc-steering-committee-bounces@haskell.org> On Behalf Of Spiwack, | > Arnaud | > Sent: 27 October 2021 09:20 | > To: Richard Eisenberg mailto:rae@richarde.dev> | > Cc: ghc-steering-committee mailto:ghc-steering-committee@haskell.org> | > 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.