every implicit form of variable binding must have an explicit equivalent

The way I understand the proposal is that the change in phrasing of the Explicit Binding Principle is largely the addition of “unambiguously” in the sentence that, regardless of the context, is unambiguously a binding site. This unambiguousness is specifically the realm of the Lexical Scoping Principle. I don't find this change useful. (in parallel, John Ericson has proposed a call with some of us to clarify the details and answer Simon's interogation, it hasn't been set up yet) /Arnaud On Wed, 21 Dec 2022 at 16:44, Simon Peyton Jones < simon.peytonjones@gmail.com> wrote:

The new Explicit Binding Principle is now somewhat stronger, in that it

...

requires that there is a form with an explicit binder which “regardless of the context, is unambiguously a binding site”. The Lexical Binding Principle is changed, as well, to refer to this new change but it's not substantial.

I personally don't think this change to the principles is valuable, it simply blurs the distinction between the Explicit Binding Principle and the Lexical Binding Principle.

I don't get this. Why is the EBP stronger? Example? I don't see why the distinction is blurred.

The changes to the principles seem fine to me -- modest but useful clarifications, no change in semantics.

I don't think I fully understand the second part about flags etc. My head spins.

I wish there was a compact summary of the actual changes proposed. I'll ask John for that.

Simon

On Wed, 14 Dec 2022 at 07:09, Arnaud Spiwack wrote:

...

Dear all,

Proposal https://github.com/ghc-proposals/ghc-proposals/pull/532 Rendered link for the proposal (although several other files are modified): https://github.com/Ericson2314/ghc-proposals/blob/type-variables/proposals/0...

John Ericson proposes to amend Richard's recent Modern Scoped Type Variables Proposal [ https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0448-ty... ]

There are two essential parts to the change: 1. The Explicit Binding Principle is modified 2. Change the two extensions introduced by Proposal #285 [ https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0285-no... ], -XImplicitForalls and -XPatternSignatureBinds (so that they can be deactivated), and consolidated in Richard's proposal (where -XPatternSignatureBinds is turned into a binding) into a single -XImplicitBinds extension

---------

The new Explicit Binding Principle is now somewhat stronger, in that it requires that there is a form with an explicit binder which “regardless of the context, is unambiguously a binding site”. The Lexical Binding Principle is changed, as well, to refer to this new change but it's not substantial.

I personally don't think this change to the principles is valuable, it simply blurs the distinction between the Explicit Binding Principle and the Lexical Binding Principle. I find the current phrasing more useful. And I don't think the semantics of the conjunction is actually changed. So I recommend that we reject the changes to the Principles.

------------

John makes a good point: `-XPatternSignature` being a warning has a limitation. This is pointed out in section “Unified Namespacing and extension monotonicity” of the patch to the Modern Scoped Type Variables Proposal. Namely that in

t = Int (x :: t) = 0

The current semantics is to have `t` be a binder (because `t` is not bound in the type namespace). If we add a warning for pattern signatures binders, `t` will still be a binder. But we are starting to introduce a new semantics where failing to lookup `t` in the type namespace, we will fall back to look it up in the term namespace instead. The current semantics of considering `t` a binder in this case is at odds with the fallback strategy. (crucially for this recommendation, the same issue occurs in signatures where `forall`-s are implicitly inferred)

(Context: At the time where #285 was proposed, I was in favour of a single extension. Simon PJ strongly pushed for two extensions.)

My inclination today is that we have a choice: we can either - consider the problem above to be a serious issue, in which case we probably want to eventually deprecate both implicit foralls and pattern signature binds. If this is the case, then they should be gated behind an extension (see also the discussion on the meaning of extensions that we're currently having). I find it healthy to have a single extension for both features because the problem that the extension is solving is the same, hence, in this case, I recommend accepting the changes. - be happy that the semantics is a little quirky, with the fallback happening only when an explicit forall is specified (and never in pattern signatures). In which case both should probably be warnings, it makes sense for the warnings to be separate categories as these are two different features. In this case I recommend rejection of the proposed changes.

------------

I realise I'm leaving a big choice hanging. It's a big decision, I think, which we should weigh carefully (which is kind of funny because the proposed change itself is rather small).

Personally, I'd be happy with all implicit foralls and pattern signature binds to be deprecated (so I'm actually taking a position I guess). But I'm not sure that it's super realistic considering the quantity of Haskell that has been written so far. I imagine that there are millions of implicit foralls on Hackage.

PS: I'll be on holiday for the next three weeks (starting on Friday night), so you'll have a little while to debate this while I'm away. _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee