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

[Simon Peyton Jones]

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.
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20240116/cff02080/attachment-0001.html>