[ghc-steering-committee] Proposal #608, -XPatternSignatureBinds. Rec: accept

Mon Jan 29 08:06:54 UTC 2024

Hi,

I had to peek at
https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0378-dependent-type-design.rst
to remind myself whether the “Local Lexical Scoping Principle” (every
mention of a variable is clearly a binder or a reference) was part of
that, or just the “Lexical Scoping Principle” is. Turns out the LLSP
isn’t part of it. But I have a vague memory that the LSP together with
the SUP is much easier when we have the LLSP?

Anyways, partly because of the dubious status and future of
ScopedTypeVariables, as a user I found myself wanting to enable the
simple part of pattern binds (do `xs :: String ← …`) without enable
other parts of that extension.

Cheers,
Joachim

Am Sonntag, dem 28.01.2024 um 18:50 -0600 schrieb Eric Seidel:
> Yep that’s the question. 
> 
> If we were starting from scratch I would agree that B is better. But I worry that there may be a lot of code out there that expects A.
> 
> So then this becomes a question of tradeoffs, is the simplification benefit of this change sufficient to justify the migration cost we may be imposing on the community? 
> 
> It seems unlikely to me.
> 
> Sent from my iPhone
> 
> > On Jan 28, 2024, at 12:22, Simon Peyton Jones <simon.peytonjones at gmail.com> wrote:
> > 
> > > When I review a proposal for a new extension, one of the
> > > questions I ask myself is "would I eventually support including this in
> > > a GHC20xx standard?" If the answer is no (and if the extension is not one
> > > of the advanced or niche things like CPP), then I'm much less likely to
> > > support it.
> > 
> > Aha.  Now I understand your point thanks.
> > 
> > In the glorious future, what do we want?
> >  * Plan A.   "A pattern signature brings into scope any variables that aren't already in scope".  It's a bit of a tricky rule. If we see `f (Just x) = rhs` we know that it brings `x` into scope regardless.  Simple.  No so with pattern-signatures!
> >    
> >  * Plan B.   Pattern signatures never bring anything into scope.  To do that, use @type patterns.  For example, instead of
> >        f (Just (x::a)) = rhs
> >    say
> >        f (Just @a x) = rhs
> >    Now it's clear that `a` is being brought into scope.
> > I lean towards Plan B, but you raise a good point.  I'd love to know what our consensus is.   RSVP steering committee members.
> > 
> > Simon
> > 
> > On Sun, 28 Jan 2024 at 00:12, Eric Seidel <eric at seidel.io> wrote:
> > > I think it's mostly a philosophical point. We have GHC2021 which is the
> > > current "blessed" version of the language. It includes ScopedTypeVariables,
> > > which if I understand correctly is a superset of PatternSigs. We also want
> > > to move in the direction of having *fewer* interacting extensions. In my
> > > mind that is one of the main motivations for introducing the GHC20xx
> > > standards. When I review a proposal for a new extension, one of the
> > > questions I ask myself is "would I eventually support including this in
> > > a GHC20xx standard?" If the answer is no (and if the extension is not one
> > > of the advanced or niche things like CPP), then I'm much less likely to
> > > support it.
> > > 
> > > So what is the purpose of refactoring extensions that are implied by
> > > ScopedTypeVariables? It seems like needless churn if ScopedTypeVariables
> > > is here to stay. On the other hand, if we mean to change ScopedTypeVariables
> > > we should be explicit about that. 
> > > 
> > > On Sat, Jan 27, 2024, at 16:56, Simon Peyton Jones wrote:
> > > > To me this looks uncontroversial.  
> > > >   • We have a currently-deprecated extension -XPatternSignatures
> > > >   • This proposal rehabilitates it (with a narrower scope than before) 
> > > > and adds a new one -XPatternSignatureBinds
> > > >   • If you don't use these extensions they won't harm you
> > > >   • The behaviour of -XScopedTypeVariables is unchanged
> > > > It's a fairly tiny thing, easy to implement, easy to document.  I don't 
> > > > care very much, but I'm content to approve it.
> > > > 
> > > > My only regret is that we don't have a "warning form" for language 
> > > > extensions (see 
> > > > https://github.com/ghc-proposals/ghc-proposals/pull/620) . I'd like to 
> > > > say -WPatternSignatureBinds, meaning to allow pattern-signatures to 
> > > > bind, but warn on every such occasion.  Lacking such a "warning form" 
> > > > we have to *also* have `-Wpattern-signature-binds`.
> > > > 
> > > > Eric, I'm not sure what specifically you are objecting to.  Are you 
> > > > making a philosophical point, or is there active harm here?
> > > > 
> > > > Simon
> > > > 
> > > > On Sat, 27 Jan 2024 at 19:44, Eric Seidel <eric at seidel.io> wrote:
> > > > > The motivation for this change does not make sense to me. ScopedTypeVariables
> > > > > is used everywhere and is even part of GHC2021. The goal of this change appears
> > > > > to be to extract out a controversial piece of PatternSignatures such that it
> > > > > could be later removed entirely, but without addressing the issue of
> > > > > ScopedTypeVariables.
> > > > > 
> > > > > That's going about it the wrong way IMO. If we want to remove the behavior
> > > > > this proposal calls PatternSignatureBinds, the Committee should first adopt
> > > > > a resolution that we will remove (or alter the meaning of) ScopedTypeVariables
> > > > > in the next GHC20xx. If we get agreement on that, then this proposal could make
> > > > > sense as a step towards the broader goal.
> > > > > 
> > > > > Outside of that broader agreement though, this feels more like a fork-inducing
> > > > > proposal and I would vote against.
> > > > > 
> > > > > On Wed, Jan 24, 2024, at 11:32, Richard Eisenberg wrote:
> > > > > > John Ericson has submitted proposal #608 
> > > > > > <https://github.com/ghc-proposals/ghc-proposals/pull/608> about adding 
> > > > > > -XPatternSignatureBinds. The proposal is an amendment and is thus a 
> > > > > > little harder to consume. I recommend reading the summary here.
> > > > > > 
> > > > > > Proposed change:
> > > > > > 
> > > > > > The proposed -XPatternSignatureBinds takes a piece out from 
> > > > > > -XPatternSignatures: with only -XPatternSignatures and not 
> > > > > > -XPatternSignatureBinds, a pattern signature  can mention in-scope type 
> > > > > > variables but can never bind fresh ones. With -XPatternSignatureBinds, 
> > > > > > an appearance of an out-of-scope type variable in a pattern signature 
> > > > > > will cause the variable to be bound to the type it unifies with.
> > > > > > 
> > > > > > -XScopedTypeVariables will imply -XPatternSignatures 
> > > > > > -XPatternSignatureBinds (and a few more), so the behavior of 
> > > > > > -XScopedTypeVariables is completely unchanged. Note that 
> > > > > > -XPatternSignatures is currently deprecated (and has been so for a long 
> > > > > > time), so a change in behavior there is not so bad.
> > > > > > 
> > > > > > Motivation for the change:
> > > > > > 
> > > > > > - It is awkward to have a rule in a language where scoping behavior 
> > > > > > depends on what else is in scope. This can confound e.g. tools meant to 
> > > > > > find the bindings sites of a variable occurrence.
> > > > > > - The implicit binding we have today plays poorly with the plan to 
> > > > > > allow users to pretend GHC has a unified namespace. That is, suppose x 
> > > > > > is in scope as a term variable, and then we have f (... :: ... x ...) = 
> > > > > > ... . Should that x be bound implicitly there or not? It's pretty 
> > > > > > unclear. By separating out -XPatternSignatureBinds from 
> > > > > > -XPatternSignatures, users of the latter are insulated from worrying 
> > > > > > about this potential future change.
> > > > > > 
> > > > > > My opinion:
> > > > > > 
> > > > > > - John has argued that this will make future namespace changes easier. 
> > > > > > I disagree with this assessment, because -XScopedTypeVariables is 
> > > > > > utterly pervasive. So the problem that this change is supposed to solve 
> > > > > > becomes only a tiny bit smaller, benefiting only those users who 
> > > > > > carefully enable -XPatternSignatures but not, say, 
> > > > > > -XScopedTypeVariables.
> > > > > > - But in the end, I don't care all that much. I've come to the opinion 
> > > > > > that we shouldn't worry about the distinction between warnings and 
> > > > > > extensions. The net effect of this proposal is to promote a warning 
> > > > > > into an extension (because we previously had 
> > > > > > -Wpattern-signature-binds). So if we shouldn't worry about this 
> > > > > > distinction, then this proposal is a no-op on the aspects of the 
> > > > > > language we should care about, and thus accepting and rejecting have 
> > > > > > the same effect. (This little analysis only makes sense because the 
> > > > > > features are so new -- there's no broad re-education to do or 
> > > > > > back-compat issues.)
> > > > > > - Accepting will make at least one person (John) happy. And I don't 
> > > > > > note anyone who would become unhappy. More happy people is more better. 
> > > > > > So I recommend acceptance. :)
> > > > > > 
> > > > > > Please let us know your thoughts!
> > > > > > Richard
> > > > > > _______________________________________________
> > > > > > ghc-steering-committee mailing list
> > > > > > ghc-steering-committee at haskell.org
> > > > > > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
> > > > > _______________________________________________
> > > > > ghc-steering-committee mailing list
> > > > > ghc-steering-committee at haskell.org
> > > > > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

-- 
Joachim Breitner
  mail at joachim-breitner.de
  http://www.joachim-breitner.de/