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

[Richard Eisenberg]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20240106/7c6c4fd7/attachment.html>