[ghc-steering-committee] Proposal #532: Clean up and simplify the treatment of implicit bindings. Recommendation: partially accept (maybe)

[Arnaud Spiwack]

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

> every implicit form of variable binding must have an explicit equivalent
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 at 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 <arnaud.spiwack at tweag.io>
> 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/0532-type-variable-scoping.rst
>>
>> John Ericson proposes to amend Richard's recent Modern Scoped Type
>> Variables Proposal [
>> https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0448-type-variable-scoping.rst
>> ]
>>
>> 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-implicit-binds.rst
>> ], -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 at haskell.org
>> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20230119/0d919129/attachment.html>