[ghc-steering-committee] Proposal #624 on linear let-bindings; recommendation: accept
Adam Gundry
adam at well-typed.com
Sat Jan 13 20:00:42 UTC 2024
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
More information about the ghc-steering-committee
mailing list