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

Mon Jan 22 09:03:46 UTC 2024

 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?

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.

Simon

On Fri, 19 Jan 2024 at 10:42, Arnaud Spiwack <arnaud.spiwack at tweag.io>
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?
>
> On Wed, 17 Jan 2024 at 22:30, Richard Eisenberg <rae at richarde.dev> wrote:
>
>> 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.
>>
>> 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.
>>
>> Richard
>>
>> On Jan 16, 2024, at 12:52 PM, Simon Peyton Jones <
>> simon.peytonjones at gmail.com> wrote:
>>
>> Richard
>>
>> Arnaud articulates some alternatives, which I am very fuzzy about (as I
>> say in my email).
>>
>> 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.)
>>
>> Simon
>>
>> On Tue, 16 Jan 2024 at 18:52, Richard Eisenberg <rae at richarde.dev> wrote:
>>
>>> 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.
>>>
>>> So I'm for the design Arnaud articulates below, but support the proposal
>>> regardless.
>>>
>>> Richard
>>>
>>> On Jan 12, 2024, at 3:08 AM, Arnaud Spiwack <arnaud.spiwack at tweag.io>
>>> wrote:
>>>
>>> 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.
>>>
>>> I'm rather agnostic on which side we choose, to be honest. Anyone with
>>> medium-to-strong opinions on the question?
>>>
>>>
>>> Restrictions of multiplicity-annotated let bindings
>>> ---------------------------------------------------
>>>
>>> The proposal specifies that a multiplicity annotated non-variable let
>>> binding ``let %p pat``
>>> must be such that ``pat = !pat'`` even if ``p = 'Many``. It is easy to
>>> lift this restriction on two dimension:
>>>
>>> - We can say, instead, that patterns not of the form ``!pat'`` emit a
>>>   ``p ~ 'Many`` constraint instead. They already do (for the sake of
>>>   inference), so this is strictly less code.
>>> - We can generalise to more strict patterns. For instance, we don't
>>>   need to require a ``!`` if ``-XStrict`` is on, we can have patterns
>>>   of the form ``(!pat')`` (with additional parentheses). This is a few
>>>   lines of codes, inference actually already does this in my
>>>   implementation, so it's already paid for (though it does annoyingly
>>>   mostly duplicate another definition of strict pattern which I
>>>   couldn't find a way to factor as a single function, I don't like
>>>   this).
>>>
>>> The reason that motivated the stronger restriction is to improve error
>>> messages, because we can then error out with “multiplicity-annotated
>>> let-bound patterns must be of the form !pat”, instead of the more
>>> mysterious “Couldn't unify 'Many with 'One”
>>> (see `#23586 <https://gitlab.haskell.org/ghc/ghc/-/issues/23586>`_).
>>> But maybe the additional restrictions are more surprising than the
>>> error messages are helpful.
>>>
>>> On Mon, 8 Jan 2024 at 10:07, Simon Peyton Jones <
>>> simon.peytonjones at gmail.com> wrote:
>>>
>>>> I support acceptance.  Let's land this soon.
>>>>
>>>> Simon
>>>>
>>>> On Sat, 6 Jan 2024 at 04:45, Richard Eisenberg <rae at richarde.dev>
>>>> wrote:
>>>>
>>>>> Hi all,
>>>>>
>>>>> I've reviewed Arnaud's
>>>>> https://github.com/ghc-proposals/ghc-proposals/pull/624 and wish to
>>>>> recommend acceptance.
>>>>>
>>>>> The proposal is an amendment to the proposal for linear types, adding
>>>>> support for linear let bindings.
>>>>>
>>>>> Today, if you have
>>>>>
>>>>> f :: T %1-> T
>>>>> f t = let t2 = t in t2
>>>>>
>>>>> 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.
>>>>>
>>>>> 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.
>>>>>
>>>>> Please share your thoughts!
>>>>>
>>>>> Thanks,
>>>>> Richard
>>>>> _______________________________________________
>>>>> ghc-steering-committee mailing list
>>>>> ghc-steering-committee at haskell.org
>>>>>
>>>>> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>>>>>
>>>> _______________________________________________
>>>> ghc-steering-committee mailing list
>>>> ghc-steering-committee at haskell.org
>>>> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>>>>
>>>
>>>
>>> --
>>> Arnaud Spiwack
>>> Director, Research at https://moduscreate.com and https://tweag.io.
>>>
>>>
>>>
>>
>
> --
> Arnaud Spiwack
> Director, Research at https://moduscreate.com and https://tweag.io.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20240122/50104e6a/attachment.html>