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

[Arnaud Spiwack]

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/b1dfc7dd/attachment-0001.html>