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

[Arnaud Spiwack]

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/240ed780/attachment.html>