[ghc-steering-committee] Proposal #624 on linear let-bindings; recommendation: accept

[Richard Eisenberg]

I find Simon's rules put too much emphasis on syntax (the appearance of a ! mark), whereas I'm arguing in favor of basing the rules on semantics (is the binding strict). But I'm happy to concede the point; I just think my proposal is actually simpler (and should be so in the implementation, but I might be wrong).

One small correction to Simon's description: this is all about non-variable patterns. A variable pattern is allowed to be linear (e.g. let %1 x = f y in ...) even without a bang or other source of strictness.

Richard

> On Jan 22, 2024, at 4:29 PM, Simon Peyton Jones <simon.peytonjones at gmail.com <mailto:simon.peytonjones at gmail.com>> wrote:
> 
> I suggest:
> A pattern pat is called banged iff it is of form !pat, or (pat) where pat is banged.
> A pattern binding pat = rhs, without a user-specified multiplicity annotation
> has multiplicity Many ifpat is not banged
> If p is banged, it gets an inferred multiplicity (somehow).
> In a pattern binding %p pat = rhs, with an explicit user-specified multiplicity annotation %p
> the pattern pat must be banged regardless of  p.
> I don't think patterns in case branches are involved.  These rules concern pattern bindings pat=rhe
> 
> Simon
> 
> On Mon, 22 Jan 2024 at 10:00, Arnaud Spiwack <arnaud.spiwack at tweag.io <mailto:arnaud.spiwack at tweag.io>> wrote:
> 
> 
> On Mon, 22 Jan 2024 at 10:04, Simon Peyton Jones <simon.peytonjones at gmail.com <mailto:simon.peytonjones at gmail.com>> wrote:
> Richard seems to be the only one with a strong opinion on this. I'm happy to implement Richard's recommendations (both in the proposal and in the code), unless there are dissenting voices? 
> 
> I am still struggling to understand the choice that you are putting before us.  I laid out my understanding last week:
> I think that the issue you are debating only arises when you, the programmer, want to explicitly annotate a let/where binding with a multiplicity.  Right?
> I think that you are saying that all bindings with a non-Many multiplicity must be strict.
> I think the choices you are identifying are:
> If the explicit annotation is Many, does the binding still need to be strict?
> If the binding needs to be strict, do we insist on an explicit ! or, if -XStrict is on can we omit that bang?
> Can I ask if my understanding is correct?
> 
> It is, with two caveats:
> - the question of whether a pattern is strict also shows up when we infer the multiplicity of an unannotated let-binding. In this case, if the non-variable pattern isn't strict, then we emit a multiplicity-must-be-Many constraint. And the same choice (should we consider some patterns as strict when they aren't annotated with `!`) arises.
> - beside the -XStrict question, there is the question of whether `(!p)` (with parentheses) is considered strict.
> 
> Here's the full logic I've considered so far (where `checkManyPattern` means: must be Many, and `return WpHole` means: no constraint on the multiplicity):
> 
>     manyIfLazy dflags lpat
>       | xopt LangExt.Strict dflags = xstrict lpat
>       | otherwise = not_xstrict lpat
>       where
>         xstrict (L _ (LazyPat _ _)) = checkManyPattern pat_ty
>         xstrict (L _ (ParPat _ _ p _)) = xstrict p
>         xstrict _ = return WpHole
> 
>         not_xstrict (L _ (BangPat _ _)) = return WpHole
>         not_xstrict (L _ (VarPat _ _)) = return WpHole
>         not_xstrict (L _ (ParPat _ _ p _)) = not_xstrict p
>         not_xstrict _ = checkManyPattern pat_ty
> 
> 
>  
> Assuming so, to me the most straightforward and conservative thing is:
> All multiplicity-annotated pattern bindings must have an explicit bang, thus   let %p !pat = rhs
> This rule is simple, direct, and explicable.  No one is going to write a multiplicity-annotated pattern binding let %Many pat = rhs, so it's not worth optimising for that case.
> 
> It's certainly the more conservative option. But Richard was arguing that it's too conservative. As for explicability: which of “the pattern must be strict” or “the pattern must be annotated with a !” is easier to explain? I'm not sure, but here's some food for thought: if we settle on “annotated with a !”, then how do we explain that patterns in case branches don't need to be annotated with a “!"?

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20240124/0eef38bc/attachment.html>