<div dir="ltr">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><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, 17 Jan 2024 at 22:30, Richard Eisenberg <<a href="mailto:rae@richarde.dev">rae@richarde.dev</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 style="overflow-wrap: break-word;">Sorry for being vague: I support emitting the constraint equating the linearity annotation to `Many` whenever the binding is of a form that linearity can't handle, with a CtOrigin that makes for a good error message.<div><br></div><div>I also support allowing bang-less patterns to be linear with -XStrict; my understanding of the specification of -XStrict is that it should mean "put bangs everywhere", so accepting bang-less patterns as linear here sounds right. My hope is that this is actually a simplification, because I would imagine there some notion of "strict binding" -- encompassing both a binding with an outer ! and any binding with -XStrict -- and then this new feature just hooks into that one.</div><div><br></div><div>Richard<br><div><div><br><blockquote type="cite"><div>On Jan 16, 2024, at 12:52 PM, Simon Peyton Jones <<a href="mailto:simon.peytonjones@gmail.com" target="_blank">simon.peytonjones@gmail.com</a>> wrote:</div><br><div><div dir="ltr"><div class="gmail_default" style="font-family:tahoma,sans-serif">Richard</div><div class="gmail_default" style="font-family:tahoma,sans-serif"><br></div><div class="gmail_default" style="font-family:tahoma,sans-serif">Arnaud articulates some alternatives, which I am very fuzzy about (as I say in my email).</div><div class="gmail_default" style="font-family:tahoma,sans-serif"><br></div><div class="gmail_default" style="font-family:tahoma,sans-serif">Can you say which alternative you support? (I'm thinking of the language design only; I'm sure we can implement whichever design we choose.)</div><div class="gmail_default" style="font-family:tahoma,sans-serif"><br></div><div class="gmail_default" style="font-family:tahoma,sans-serif">Simon<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, 16 Jan 2024 at 18:52, Richard Eisenberg <<a href="mailto:rae@richarde.dev" target="_blank">rae@richarde.dev</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>I say we have our cake and eat it, too: get better inference and better error messages. I think this shouldn't be all that hard: when emitting the constraint that the linearity of the binding is `Many`, use an appropriate `CtOrigin` that can render as an informative message. I haven't gone through the code to see exactly the best structure here, but I feel pretty confident that this should be straightforward.<div><br></div><div>So I'm for the design Arnaud articulates below, but support the proposal regardless.</div><div><br></div><div>Richard<br><div><br><blockquote type="cite"><div>On Jan 12, 2024, at 3:08 AM, Arnaud Spiwack <<a href="mailto:arnaud.spiwack@tweag.io" target="_blank">arnaud.spiwack@tweag.io</a>> wrote:</div><br><div><div dir="ltr"><div>At Richard's prompting, I've added the following alternative to the proposal (the current proposal is the most conservative of the two, which we can choose to stick to if we're unsure). I'm copying the alternative here because rendering seems to be broken on Github right now.</div><div><br></div><div>I'm rather agnostic on which side we choose, to be honest. Anyone with medium-to-strong opinions on the question?<br></div><div><br></div><div><br></div><div>Restrictions of multiplicity-annotated let bindings<br>---------------------------------------------------<br><br>The proposal specifies that a multiplicity annotated non-variable let binding ``let %p pat``<br>must be such that ``pat = !pat'`` even if ``p = 'Many``. It is easy to<br>lift this restriction on two dimension:<br><br>- We can say, instead, that patterns not of the form ``!pat'`` emit a<br> ``p ~ 'Many`` constraint instead. They already do (for the sake of<br> inference), so this is strictly less code.<br>- We can generalise to more strict patterns. For instance, we don't<br> need to require a ``!`` if ``-XStrict`` is on, we can have patterns<br> of the form ``(!pat')`` (with additional parentheses). This is a few<br> lines of codes, inference actually already does this in my<br> implementation, so it's already paid for (though it does annoyingly<br> mostly duplicate another definition of strict pattern which I<br> couldn't find a way to factor as a single function, I don't like<br> this).<br><br>The reason that motivated the stronger restriction is to improve error<br>messages, because we can then error out with “multiplicity-annotated<br>let-bound patterns must be of the form !pat”, instead of the more<br>mysterious “Couldn't unify 'Many with 'One”<br>(see `#23586 <<a href="https://gitlab.haskell.org/ghc/ghc/-/issues/23586" target="_blank">https://gitlab.haskell.org/ghc/ghc/-/issues/23586</a>>`_).<br>But maybe the additional restrictions are more surprising than the<br>error messages are helpful.</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, 8 Jan 2024 at 10:07, Simon Peyton Jones <<a href="mailto:simon.peytonjones@gmail.com" target="_blank">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 class="gmail_default" style="font-family:tahoma,sans-serif">I support acceptance. Let's land this soon.</div><div class="gmail_default" style="font-family:tahoma,sans-serif"><br></div><div class="gmail_default" style="font-family:tahoma,sans-serif">Simon<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, 6 Jan 2024 at 04:45, Richard Eisenberg <<a href="mailto:rae@richarde.dev" target="_blank">rae@richarde.dev</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>Hi all,<div><br></div><div>I've reviewed Arnaud's <a href="https://github.com/ghc-proposals/ghc-proposals/pull/624" target="_blank">https://github.com/ghc-proposals/ghc-proposals/pull/624</a> and wish to recommend acceptance.</div><div><br></div><div>The proposal is an amendment to the proposal for linear types, adding support for linear let bindings.</div><div><br></div><div>Today, if you have</div><div><br></div><div>f :: T %1-> T</div><div>f t = let t2 = t in t2</div><div><br></div><div>you'll get an error because t2 is not linear. The only way to bind a linear variable is via a `case`, never a `let` or `where`. This is annoying. With this proposal, the little program above is accepted, with an inferred linearity restriction on t2. Users can also annotated their lets like `let %1 x = ... in ...`. Bindings in `where` clauses can also be inferred or annotated as linear.</div><div><br></div><div>There is a downside, of course: linear bindings have various restrictions, chiefly that they must be strict bindings (because projections are hard with linear types) and that bindings cannot be generalized. I'm a little unsure that the choices in the proposal (particularly around generalization) are the best for users, but I think the best way to learn is to experiment. In my understanding, the community knows that -XLinearTypes is subject to revision, and so I think we should just blast ahead, revising if and when necessary.</div><div><br></div><div>Please share your thoughts!</div><div><br></div><div>Thanks,</div><div>Richard</div></div>_______________________________________________<br>
ghc-steering-committee mailing list<br>
<a href="mailto:ghc-steering-committee@haskell.org" target="_blank">ghc-steering-committee@haskell.org</a><br>
<a href="https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee" rel="noreferrer" target="_blank">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee</a><br>
</blockquote></div>
_______________________________________________<br>
ghc-steering-committee mailing list<br>
<a href="mailto:ghc-steering-committee@haskell.org" target="_blank">ghc-steering-committee@haskell.org</a><br>
<a href="https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee" rel="noreferrer" target="_blank">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee</a><br>
</blockquote></div><br clear="all"><br><span class="gmail_signature_prefix">-- </span><br><div dir="ltr" class="gmail_signature"><div dir="ltr">Arnaud Spiwack<br>Director, Research at <a href="https://moduscreate.com/" rel="noopener noreferrer" target="_blank">https://moduscreate.com</a> and <a href="https://tweag.io/" rel="noopener noreferrer" target="_blank">https://tweag.io</a>.</div></div>
</div></blockquote></div><br></div></div></blockquote></div>
</div></blockquote></div><br></div></div></div></blockquote></div><br clear="all"><br><span class="gmail_signature_prefix">-- </span><br><div dir="ltr" class="gmail_signature"><div dir="ltr">Arnaud Spiwack<br>Director, Research at <a href="https://moduscreate.com" rel="noopener noreferrer" target="_blank">https://moduscreate.com</a> and <a href="https://tweag.io" rel="noopener noreferrer" target="_blank">https://tweag.io</a>.</div></div>