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

[Simon Peyton Jones]

I do not feel strongly. I am content for Arnaud to make a choice, and make
sure that it is clearly expressed in the final version of the spec.

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.


I did not know that.   Can the proposal spell this out explicitly please?

Do newtypes make a difference?  E.g      let N x = e in ...
where N is the data contructor of a newtype?

Simon

On Wed, 24 Jan 2024 at 14:07, Richard Eisenberg <rae at richarde.dev> wrote:

> 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> 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>
> 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/20240124/576a5491/attachment-0001.html>