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

[Simon Peyton Jones]

I do not feel strongly.   Simpler is better.

It would be great to settle this proposal asap

-----------

BTW: proposals are not formatting for me: I just get shown the raw RST
file  E.g
https://github.com/tweag/ghc-proposals/blob/linear-lets/proposals/0111-linear-types.rst

What am I doing wrong?

Simon

On Fri, 12 Jan 2024 at 10:08, 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/20240112/79535aad/attachment.html>