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

[Simon Peyton Jones]

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>
wrote:

>
>
> On Mon, 22 Jan 2024 at 10:04, Simon Peyton Jones <
> 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/20240122/652231c4/attachment.html>