<div dir="ltr"><div dir="ltr"><br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, 22 Jan 2024 at 10:04, Simon Peyton Jones <<a href="mailto:simon.peytonjones@gmail.com">simon.peytonjones@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div style="font-family:tahoma,sans-serif">
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? <br></div><div style="font-family:tahoma,sans-serif"><br></div><div style="font-family:tahoma,sans-serif">I am still struggling to understand the choice that you are putting before us.  I laid out my understanding last week:</div><div style="font-family:tahoma,sans-serif"></div><div style="font-family:tahoma,sans-serif">
<ul><li>I think that the issue you are debating only arises when you, the programmer, want to <b>explicitly annotate </b>a let/where binding with a multiplicity.  Right?<br></li><li>I think that you are saying that all bindings with a <b>non-Many </b>multiplicity <b>must </b>be strict.</li><li>I think the choices you are identifying are:</li><ul><li>If the explicit annotation is Many, does the binding still need to be strict?</li><li>If the binding needs to be strict, do we insist on an explicit ! or, if -XStrict is on can we omit that bang?</li></ul></ul><div>Can I ask if my understanding is correct?</div></div></div></blockquote><div><br></div><div>It is, with two caveats:</div><div>- 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.</div><div>- beside the -XStrict question, there is the question of whether `(!p)` (with parentheses) is considered strict.</div><div><br></div><div>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):</div><div><br></div><div>    manyIfLazy dflags lpat<br>      | xopt LangExt.Strict dflags = xstrict lpat<br>      | otherwise = not_xstrict lpat<br>      where<br>        xstrict (L _ (LazyPat _ _)) = checkManyPattern pat_ty<br>        xstrict (L _ (ParPat _ _ p _)) = xstrict p<br>        xstrict _ = return WpHole<br><br>        not_xstrict (L _ (BangPat _ _)) = return WpHole<br>        not_xstrict (L _ (VarPat _ _)) = return WpHole<br>        not_xstrict (L _ (ParPat _ _ p _)) = not_xstrict p<br>        not_xstrict _ = checkManyPattern pat_ty</div><div><br></div><div><br></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div style="font-family:tahoma,sans-serif"><div></div><div>Assuming so, to me the most straightforward and conservative thing is:</div><div><ul><li>All multiplicity-annotated pattern bindings must have an explicit bang, thus   let %p !pat = rhs</li></ul><div>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.</div></div></div></div></blockquote><div><br></div><div>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 “!"?<br></div></div></div>