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

Simon Peyton Jones simon.peytonjones at gmail.com
Tue Jan 16 09:58:55 UTC 2024 

Arnaud, I'm sorry but I'm not close enough to this proposal to understand
the alternatives.


   - 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?

Are those the choices you are putting before us?  It would help just to lay
it out soe that even people who aren't close to linear types can have a
chance to contribute.  Otherwise we'll end up with silence, which is not
helpful to you.

Perhaps also this debate can be on the GitHub thread, rather than the
mailing list.

Simon

On Mon, 15 Jan 2024 at 15:01, Arnaud Spiwack <arnaud.spiwack at tweag.io>
wrote:

> What's simplest is not obvious.
>
> - Only accepting concrete `!pat` if there's a %p gives simpler error
> messages, but is a few lines of code extra (and you may end up with lets
> that are inferred linear but you can't add `let %1` on them if the
> inference algorithm uses a more clever definition of strict)
> - Considering a pattern as strict when `-XStrict` or in brackets, is a few
> extra lines of code but maybe more intuitive.
>
> In any case, I consider all these choices to be quite comparable in
> simplicity from a code perspective (and for the record, the least amount of
> work for me is to use both alternatives, because they're the version that
> I've already implemented). What does the user consider simplest?
>
> On Sat, 13 Jan 2024 at 21:00, Adam Gundry <adam at well-typed.com> wrote:
>
>> I haven't looked at this closely, but I'm happy to trust Arnaud and
>> Richard's judgment and accept, especially since LinearTypes is at a very
>> experimental stage.
>>
>> Adam
>>
>>
>> On 12/01/2024 10:08, Arnaud Spiwack 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
>> > <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 <mailto: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
>> >     <mailto:rae at richarde.dev>> wrote:
>> >
>> >         Hi all,
>> >
>> >         I've reviewed Arnaud's
>> >         https://github.com/ghc-proposals/ghc-proposals/pull/624
>> >         <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
>>
>>
>> --
>> Adam Gundry, Haskell Consultant
>> Well-Typed LLP, https://www.well-typed.com/
>>
>> Registered in England & Wales, OC335890
>> 27 Old Gloucester Street, London WC1N 3AX, England
>>
>> _______________________________________________
>> 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.
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20240116/936f8803/attachment-0001.html>

More information about the ghc-steering-committee mailing list