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

[Simon Peyton Jones]

>
> 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/20221221/9d2d3643/attachment-0001.html>