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.