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 wrote:

I support acceptance. Let's land this soon.

Simon

On Sat, 6 Jan 2024 at 04:45, Richard Eisenberg 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@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@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.

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 mailto:simon.peytonjones@gmail.com> wrote:

I support acceptance.  Let's land this soon.

Simon

On Sat, 6 Jan 2024 at 04:45, Richard Eisenberg mailto:rae@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

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 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 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 mailto:simon.peytonjones@gmail.com> wrote:

I support acceptance. Let's land this soon.

Simon

On Sat, 6 Jan 2024 at 04:45, Richard Eisenberg mailto:rae@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@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@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Richard Arnaud articulates some alternatives, which I am very fuzzy about (as I say in my email). Can you say which alternative you support? (I'm thinking of the language design only; I'm sure we can implement whichever design we choose.) Simon On Tue, 16 Jan 2024 at 18:52, Richard Eisenberg wrote:

I say we have our cake and eat it, too: get better inference and better error messages. I think this shouldn't be all that hard: when emitting the constraint that the linearity of the binding is `Many`, use an appropriate `CtOrigin` that can render as an informative message. I haven't gone through the code to see exactly the best structure here, but I feel pretty confident that this should be straightforward.

So I'm for the design Arnaud articulates below, but support the proposal regardless.

Richard

On Jan 12, 2024, at 3:08 AM, 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`_). 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@gmail.com> wrote:

...

I support acceptance. Let's land this soon.

Simon

On Sat, 6 Jan 2024 at 04:45, Richard Eisenberg 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@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@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.

Richard seems to be the only one with a strong opinion on this. I'm happy to implement Richard's recommendations (both in the proposal and in the code), unless there are dissenting voices? On Wed, 17 Jan 2024 at 22:30, Richard Eisenberg wrote:

Sorry for being vague: I support emitting the constraint equating the linearity annotation to `Many` whenever the binding is of a form that linearity can't handle, with a CtOrigin that makes for a good error message.

I also support allowing bang-less patterns to be linear with -XStrict; my understanding of the specification of -XStrict is that it should mean "put bangs everywhere", so accepting bang-less patterns as linear here sounds right. My hope is that this is actually a simplification, because I would imagine there some notion of "strict binding" -- encompassing both a binding with an outer ! and any binding with -XStrict -- and then this new feature just hooks into that one.

Richard

On Jan 16, 2024, at 12:52 PM, Simon Peyton Jones < simon.peytonjones@gmail.com> wrote:

Richard

Arnaud articulates some alternatives, which I am very fuzzy about (as I say in my email).

Can you say which alternative you support? (I'm thinking of the language design only; I'm sure we can implement whichever design we choose.)

Simon

On Tue, 16 Jan 2024 at 18:52, Richard Eisenberg wrote:

...

I say we have our cake and eat it, too: get better inference and better error messages. I think this shouldn't be all that hard: when emitting the constraint that the linearity of the binding is `Many`, use an appropriate `CtOrigin` that can render as an informative message. I haven't gone through the code to see exactly the best structure here, but I feel pretty confident that this should be straightforward.

So I'm for the design Arnaud articulates below, but support the proposal regardless.

Richard

On Jan 12, 2024, at 3:08 AM, 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`_). 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@gmail.com> wrote:

...

I support acceptance. Let's land this soon.

Simon

On Sat, 6 Jan 2024 at 04:45, Richard Eisenberg 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@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@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.

-- Arnaud Spiwack Director, Research at https://moduscreate.com and https://tweag.io.

Richard seems to be the only one with a strong opinion on this. I'm happy to implement Richard's recommendations (both in the proposal and in the code), unless there are dissenting voices? I am still struggling to understand the choice that you are putting before us. I laid out my understanding last week: - 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? Can I ask if my understanding is correct? Assuming so, to me the most straightforward and conservative thing is: - All multiplicity-annotated pattern bindings must have an explicit bang, thus let %p !pat = rhs This rule is simple, direct, and explicable. No one is going to write a multiplicity-annotated pattern binding let %Many pat = rhs, so it's not worth optimising for that case. Simon On Fri, 19 Jan 2024 at 10:42, Arnaud Spiwack wrote:

Richard seems to be the only one with a strong opinion on this. I'm happy to implement Richard's recommendations (both in the proposal and in the code), unless there are dissenting voices?

On Wed, 17 Jan 2024 at 22:30, Richard Eisenberg wrote:

...

Sorry for being vague: I support emitting the constraint equating the linearity annotation to `Many` whenever the binding is of a form that linearity can't handle, with a CtOrigin that makes for a good error message.

I also support allowing bang-less patterns to be linear with -XStrict; my understanding of the specification of -XStrict is that it should mean "put bangs everywhere", so accepting bang-less patterns as linear here sounds right. My hope is that this is actually a simplification, because I would imagine there some notion of "strict binding" -- encompassing both a binding with an outer ! and any binding with -XStrict -- and then this new feature just hooks into that one.

Richard

On Jan 16, 2024, at 12:52 PM, Simon Peyton Jones < simon.peytonjones@gmail.com> wrote:

Richard

Arnaud articulates some alternatives, which I am very fuzzy about (as I say in my email).

Can you say which alternative you support? (I'm thinking of the language design only; I'm sure we can implement whichever design we choose.)

Simon

On Tue, 16 Jan 2024 at 18:52, Richard Eisenberg wrote:

...

I say we have our cake and eat it, too: get better inference and better error messages. I think this shouldn't be all that hard: when emitting the constraint that the linearity of the binding is `Many`, use an appropriate `CtOrigin` that can render as an informative message. I haven't gone through the code to see exactly the best structure here, but I feel pretty confident that this should be straightforward.

So I'm for the design Arnaud articulates below, but support the proposal regardless.

Richard

On Jan 12, 2024, at 3:08 AM, 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`_). 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@gmail.com> wrote:

...

I support acceptance. Let's land this soon.

Simon

On Sat, 6 Jan 2024 at 04:45, Richard Eisenberg 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@haskell.org

https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@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.

-- Arnaud Spiwack Director, Research at https://moduscreate.com and https://tweag.io.

I suggest: - A pattern pat is called *banged *iff it is of form !pat, or (pat) where pat is banged. - A pattern binding pat = rhs, *without a user-specified multiplicity annotation* - has multiplicity Many ifpat is not banged - If p is banged, it gets an inferred multiplicity (somehow). - In a pattern binding %p pat = rhs, *with an explicit user-specified multiplicity annotation %p* - the pattern pat must be banged regardless of p. I don't think patterns in case branches are involved. These rules concern pattern bindings pat=rhe Simon On Mon, 22 Jan 2024 at 10:00, Arnaud Spiwack wrote:

On Mon, 22 Jan 2024 at 10:04, Simon Peyton Jones < simon.peytonjones@gmail.com> wrote:

...

Richard seems to be the only one with a strong opinion on this. I'm happy to implement Richard's recommendations (both in the proposal and in the code), unless there are dissenting voices?

I am still struggling to understand the choice that you are putting before us. I laid out my understanding last week:

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

Can I ask if my understanding is correct?

It is, with two caveats: - the question of whether a pattern is strict also shows up when we infer the multiplicity of an unannotated let-binding. In this case, if the non-variable pattern isn't strict, then we emit a multiplicity-must-be-Many constraint. And the same choice (should we consider some patterns as strict when they aren't annotated with `!`) arises. - beside the -XStrict question, there is the question of whether `(!p)` (with parentheses) is considered strict.

Here's the full logic I've considered so far (where `checkManyPattern` means: must be Many, and `return WpHole` means: no constraint on the multiplicity):

manyIfLazy dflags lpat | xopt LangExt.Strict dflags = xstrict lpat | otherwise = not_xstrict lpat where xstrict (L _ (LazyPat _ _)) = checkManyPattern pat_ty xstrict (L _ (ParPat _ _ p _)) = xstrict p xstrict _ = return WpHole

not_xstrict (L _ (BangPat _ _)) = return WpHole not_xstrict (L _ (VarPat _ _)) = return WpHole not_xstrict (L _ (ParPat _ _ p _)) = not_xstrict p not_xstrict _ = checkManyPattern pat_ty

...

Assuming so, to me the most straightforward and conservative thing is:

- All multiplicity-annotated pattern bindings must have an explicit bang, thus let %p !pat = rhs

This rule is simple, direct, and explicable. No one is going to write a multiplicity-annotated pattern binding let %Many pat = rhs, so it's not worth optimising for that case.

It's certainly the more conservative option. But Richard was arguing that it's too conservative. As for explicability: which of “the pattern must be strict” or “the pattern must be annotated with a !” is easier to explain? I'm not sure, but here's some food for thought: if we settle on “annotated with a !”, then how do we explain that patterns in case branches don't need to be annotated with a “!"?

I do not feel strongly. I am content for Arnaud to make a choice, and make sure that it is clearly expressed in the final version of the spec. One small correction to Simon's description: this is all about non-variable

patterns. A variable pattern is allowed to be linear (e.g. let %1 x = f y in ...) even without a bang or other source of strictness.

I did not know that. Can the proposal spell this out explicitly please? Do newtypes make a difference? E.g let N x = e in ... where N is the data contructor of a newtype? Simon On Wed, 24 Jan 2024 at 14:07, Richard Eisenberg wrote:

I find Simon's rules put too much emphasis on syntax (the appearance of a ! mark), whereas I'm arguing in favor of basing the rules on semantics (is the binding strict). But I'm happy to concede the point; I just think my proposal is actually simpler (and should be so in the implementation, but I might be wrong).

One small correction to Simon's description: this is all about non-variable patterns. A variable pattern is allowed to be linear (e.g. let %1 x = f y in ...) even without a bang or other source of strictness.

Richard

On Jan 22, 2024, at 4:29 PM, Simon Peyton Jones < simon.peytonjones@gmail.com> wrote:

I suggest:

- A pattern pat is called *banged *iff it is of form !pat, or (pat) where pat is banged. - A pattern binding pat = rhs, *without a user-specified multiplicity annotation* - has multiplicity Many ifpat is not banged - If p is banged, it gets an inferred multiplicity (somehow). - In a pattern binding %p pat = rhs, *with an explicit user-specified multiplicity annotation %p* - the pattern pat must be banged regardless of p.

I don't think patterns in case branches are involved. These rules concern pattern bindings pat=rhe

Simon

On Mon, 22 Jan 2024 at 10:00, Arnaud Spiwack wrote:

...

On Mon, 22 Jan 2024 at 10:04, Simon Peyton Jones < simon.peytonjones@gmail.com> wrote:

...

Richard seems to be the only one with a strong opinion on this. I'm happy to implement Richard's recommendations (both in the proposal and in the code), unless there are dissenting voices?

I am still struggling to understand the choice that you are putting before us. I laid out my understanding last week:

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

Can I ask if my understanding is correct?

It is, with two caveats: - the question of whether a pattern is strict also shows up when we infer the multiplicity of an unannotated let-binding. In this case, if the non-variable pattern isn't strict, then we emit a multiplicity-must-be-Many constraint. And the same choice (should we consider some patterns as strict when they aren't annotated with `!`) arises. - beside the -XStrict question, there is the question of whether `(!p)` (with parentheses) is considered strict.

Here's the full logic I've considered so far (where `checkManyPattern` means: must be Many, and `return WpHole` means: no constraint on the multiplicity):

manyIfLazy dflags lpat | xopt LangExt.Strict dflags = xstrict lpat | otherwise = not_xstrict lpat where xstrict (L _ (LazyPat _ _)) = checkManyPattern pat_ty xstrict (L _ (ParPat _ _ p _)) = xstrict p xstrict _ = return WpHole

not_xstrict (L _ (BangPat _ _)) = return WpHole not_xstrict (L _ (VarPat _ _)) = return WpHole not_xstrict (L _ (ParPat _ _ p _)) = not_xstrict p not_xstrict _ = checkManyPattern pat_ty

...

Assuming so, to me the most straightforward and conservative thing is:

- All multiplicity-annotated pattern bindings must have an explicit bang, thus let %p !pat = rhs

This rule is simple, direct, and explicable. No one is going to write a multiplicity-annotated pattern binding let %Many pat = rhs, so it's not worth optimising for that case.

It's certainly the more conservative option. But Richard was arguing that it's too conservative. As for explicability: which of “the pattern must be strict” or “the pattern must be annotated with a !” is easier to explain? I'm not sure, but here's some food for thought: if we settle on “annotated with a !”, then how do we explain that patterns in case branches don't need to be annotated with a “!"?

I'll have to recuse myself from this, as much of this is currently going above my head. My overall understanding is that this mostly relaxes what we accept, and therefore won't break existing code? Best, Moritz On Thu, 25 Jan 2024 at 00:39, Arnaud Spiwack wrote:

On Wed, 24 Jan 2024 at 16:39, Simon Peyton Jones < simon.peytonjones@gmail.com> wrote:

...

Do newtypes make a difference? E.g let N x = e in ... where N is the data contructor of a newtype?

I don't think it has too. So for the moment, I vote to stick to the current proposal and consider this like all lazy non-variable patterns: must be unrestricted.

I suspect that there's a possible refinement where we say that a happy pattern is either: - A variable - Strict - A newtype constructor where the inner pattern is happy.

(then if pat is an unhappy pattern, `let pat` must be unrestricted).

But I don't think I'm quite ready to go there for the time being, and that'll be a backward compatible change if we change our mind. _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Arnaud, I agree that _we_ consider LinearTypes experimental. I hope we can get https://github.com/ghc-proposals/ghc-proposals/pull/617 agreed on soon, so that the compiler has this knowledge as well. I am however not able to fully comprehend the technical details of this proposal right and therefore will defer to others on this! On Thu, 25 Jan 2024 at 16:01, Arnaud Spiwack wrote:

Moritz: there's one breakage introduced (but only for users of LinearTypes, which is considered experimental), namely that LinearTypes is proposed to now imply MonoLocalBinds.

On Thu, 25 Jan 2024 at 07:18, Moritz Angermann wrote:

...

I'll have to recuse myself from this, as much of this is currently going above my head. My overall understanding is that this mostly relaxes what we accept, and therefore won't break existing code?

Best, Moritz

On Thu, 25 Jan 2024 at 00:39, Arnaud Spiwack wrote:

...

On Wed, 24 Jan 2024 at 16:39, Simon Peyton Jones < simon.peytonjones@gmail.com> wrote:

...

Do newtypes make a difference? E.g let N x = e in ... where N is the data contructor of a newtype?

I don't think it has too. So for the moment, I vote to stick to the current proposal and consider this like all lazy non-variable patterns: must be unrestricted.

I suspect that there's a possible refinement where we say that a happy pattern is either: - A variable - Strict - A newtype constructor where the inner pattern is happy.

(then if pat is an unhappy pattern, `let pat` must be unrestricted).

But I don't think I'm quite ready to go there for the time being, and that'll be a backward compatible change if we change our mind. _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@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.

I'd like to declare this proposal accepted-modulo-tweaks. That is, I'd like to say that we'll accept this proposal, with the understanding that Arnaud and I will work out any remaining design details (as discussed in this thread), including a clear, unambiguous bit of documentation in the user manual and an update proposal. The patch implementing this change (already merged!) has some documentation, but it doesn't accurately reflect the implementation, and so a further patch will be necessary. I can review that further patch, focusing on the documentation piece.

I support this. Simon On Mon, 12 Feb 2024 at 15:02, Richard Eisenberg wrote:

Summarizing the discussion:

- Only a few have us have joined in. I'll take that as a signal that most don't have an opinion. - There is some design wiggle-room. But there seem to be few strong opinions about how to set the knobs. - Moritz is concerned about backward compatibility, given that there may not be wide knowledge in the community that -XLinearTypes is experimental.

While I agree it is regrettable that GHC itself has no built-in notion of "experimental", I'm not particularly moved by Moritz's concern here (sorry, Moritz!) -- I wager that LinearTypes is known to be pretty new and with sharp edges, and I'm pretty relaxed about changing it. We should prioritize cleaning this up so that we can be clearer in the future about what's experimental and what's not. To be clear, I think backward compatibility / stability is essential for GHC/Haskell, but I also think that until we have these notions baked into GHC (which we should do post-haste), we can use our judgement to determine that this change would not violate most users' assumptions of stability.

I'd like to declare this proposal accepted-modulo-tweaks. That is, I'd like to say that we'll accept this proposal, with the understanding that Arnaud and I will work out any remaining design details (as discussed in this thread), including a clear, unambiguous bit of documentation in the user manual and an update proposal. The patch implementing this change (already merged!) has some documentation, but it doesn't accurately reflect the implementation, and so a further patch will be necessary. I can review that further patch, focusing on the documentation piece.

Any objections to this plan?

Thanks, Richard

On Jan 25, 2024, at 3:07 AM, Moritz Angermann wrote:

Arnaud, I agree that _we_ consider LinearTypes experimental. I hope we can get https://github.com/ghc-proposals/ghc-proposals/pull/617 agreed on soon, so that the compiler has this knowledge as well. I am however not able to fully comprehend the technical details of this proposal right and therefore will defer to others on this!

On Thu, 25 Jan 2024 at 16:01, Arnaud Spiwack wrote:

...

Moritz: there's one breakage introduced (but only for users of LinearTypes, which is considered experimental), namely that LinearTypes is proposed to now imply MonoLocalBinds.

On Thu, 25 Jan 2024 at 07:18, Moritz Angermann < moritz.angermann@gmail.com> wrote:

...

I'll have to recuse myself from this, as much of this is currently going above my head. My overall understanding is that this mostly relaxes what we accept, and therefore won't break existing code?

Best, Moritz

On Thu, 25 Jan 2024 at 00:39, Arnaud Spiwack wrote:

...

On Wed, 24 Jan 2024 at 16:39, Simon Peyton Jones < simon.peytonjones@gmail.com> wrote:

...

Do newtypes make a difference? E.g let N x = e in ... where N is the data contructor of a newtype?

I don't think it has too. So for the moment, I vote to stick to the current proposal and consider this like all lazy non-variable patterns: must be unrestricted.

I suspect that there's a possible refinement where we say that a happy pattern is either: - A variable - Strict - A newtype constructor where the inner pattern is happy.

(then if pat is an unhappy pattern, `let pat` must be unrestricted).

But I don't think I'm quite ready to go there for the time being, and that'll be a backward compatible change if we change our mind. _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@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@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee