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
| 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.
