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

[Adam Gundry]

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