<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><meta http-equiv="Content-Type" content="text/html; charset=utf-8" class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><meta http-equiv="Content-Type" content="text/html; charset=utf-8" class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">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).<div class=""><br class=""></div><div class="">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.</div><div class=""><br class=""></div><div class="">Richard<br class=""><div class=""><br class=""><blockquote type="cite" class=""><div class="">On Jan 22, 2024, at 4:29 PM, Simon Peyton Jones <<a href="mailto:simon.peytonjones@gmail.com" class="">simon.peytonjones@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class=""><div class="gmail_default" style="font-family:tahoma,sans-serif">I suggest:</div><div class="gmail_default" style="font-family:tahoma,sans-serif"><ul class=""><li class="">A pattern pat is called <b class="">banged </b>iff it is of form !pat, or (pat) where pat is banged.</li><li class="">A pattern binding pat = rhs, <b class="">without a user-specified multiplicity annotation</b></li><ul class=""><li class="">has multiplicity Many ifpat is not banged</li><li class="">If p is banged, it gets an inferred multiplicity (somehow).</li></ul><li class="">In a pattern binding %p pat = rhs, <b class="">with an explicit user-specified multiplicity annotation %p</b></li><ul class=""><li class="">the pattern pat must be banged regardless of p.</li></ul></ul><div class="">I don't think patterns in case branches are involved. These rules concern pattern bindings pat=rhe</div><div class=""><br class=""></div><div class="">Simon<br class=""></div></div></div><br class=""><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, 22 Jan 2024 at 10:00, Arnaud Spiwack <<a href="mailto:arnaud.spiwack@tweag.io" class="">arnaud.spiwack@tweag.io</a>> wrote:<br class=""></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" class=""><div dir="ltr" class=""><br class=""></div><br class=""><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" target="_blank" class="">simon.peytonjones@gmail.com</a>> wrote:<br class=""></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" class=""><div style="font-family:tahoma,sans-serif" class="">
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 class=""></div><div style="font-family:tahoma,sans-serif" class=""><br class=""></div><div style="font-family:tahoma,sans-serif" class="">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" class=""></div><div style="font-family:tahoma,sans-serif" class="">
<ul class=""><li class="">I think that the issue you are debating only arises when you, the programmer, want to <b class="">explicitly annotate </b>a let/where binding with a multiplicity. Right?<br class=""></li><li class="">I think that you are saying that all bindings with a <b class="">non-Many </b>multiplicity <b class="">must </b>be strict.</li><li class="">I think the choices you are identifying are:</li><ul class=""><li class="">If the explicit annotation is Many, does the binding still need to be strict?</li><li class="">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 class="">Can I ask if my understanding is correct?</div></div></div></blockquote><div class=""><br class=""></div><div class="">It is, with two caveats:</div><div class="">- 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 class="">- beside the -XStrict question, there is the question of whether `(!p)` (with parentheses) is considered strict.</div><div class=""><br class=""></div><div class="">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 class=""><br class=""></div><div class=""> manyIfLazy dflags lpat<br class=""> | xopt LangExt.Strict dflags = xstrict lpat<br class=""> | otherwise = not_xstrict lpat<br class=""> where<br class=""> xstrict (L _ (LazyPat _ _)) = checkManyPattern pat_ty<br class=""> xstrict (L _ (ParPat _ _ p _)) = xstrict p<br class=""> xstrict _ = return WpHole<br class=""><br class=""> not_xstrict (L _ (BangPat _ _)) = return WpHole<br class=""> not_xstrict (L _ (VarPat _ _)) = return WpHole<br class=""> not_xstrict (L _ (ParPat _ _ p _)) = not_xstrict p<br class=""> not_xstrict _ = checkManyPattern pat_ty</div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""> </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" class=""><div style="font-family:tahoma,sans-serif" class=""><div class=""></div><div class="">Assuming so, to me the most straightforward and conservative thing is:</div><div class=""><ul class=""><li class="">All multiplicity-annotated pattern bindings must have an explicit bang, thus let %p !pat = rhs</li></ul><div class="">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 class=""><br class=""></div><div class="">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 class=""></div></div></div>
</blockquote></div>
</div></blockquote></div><br class=""></div></div></div></body></html>