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

Fri Jan 19 10:42:18 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?

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/20240119/5ac10e53/attachment.html>