#621: Linear constraints, recommendation: accept

Jakob Brünker

14 Jan 2025 14 Jan '25

5:45 p.m.

Dear committee, Arnaud Spiwack and Jack Hughes propose to introduce linear constraints. These work analogously to linear functions - as can be seen with the new syntax, which is %1 =>, reflecting the existing %1 ->. The motivation is that these constraints make it possible to design linearly typed APIs that are more convenient to use: Without the linear constraints, tokens would have to be passed manually into each function in these cases. The proposal also introduces dupable classes, which can be used multiple times even when they appear in a linear context, but cannot be passed to an unrestricted function. This is necessary to make some API designs work, see the proposal for details. To me, it seems that this proposal or something like it is necessary to unlock the full potential of linear types. The proposal lays out why monadic API designs don't provide the same benefits, and while there are potential future GHC developments that could make using it even more convenient (existential types, strict let improvements; see proposal), I believe it would already be sufficiently useful with today's GHC to be a valuable addition. Thus, I recommend acceptance. Please read through the proposal and voice your opinions. Best, Jakob

Attachments:

attachment.html (text/html — 1.4 KB)

Show replies by date

Sebastian Graf

20 Jan 20 Jan

4:22 a.m.

New subject: #621: Linear constraints, recommendation: accept

I vote to return the proposal for revision. I listed my feedback in the thread https://github.com/ghc-proposals/ghc-proposals/pull/621#issuecomment-2601848..., but the gist is: While I am sympathetic to the goal of introducing linearity annotations to

...

constraints, simply because it is a logical extension of -XLinearTypes, I am afraid I do not feel motivated after having considered the examples in the proposal.

In fact, I think the examples overpromise on the utility of linear

...

constraints and the problems it solves have simpler, more direct solutions.

Cheers, Sebastian Am Di., 14. Jan. 2025 um 23:45 Uhr schrieb Jakob Brünker < jakob.bruenker@gmail.com>:

...

Dear committee,

Arnaud Spiwack and Jack Hughes propose to introduce linear constraints.

These work analogously to linear functions - as can be seen with the new syntax, which is %1 =>, reflecting the existing %1 ->. The motivation is that these constraints make it possible to design linearly typed APIs that are more convenient to use: Without the linear constraints, tokens would have to be passed manually into each function in these cases.

The proposal also introduces dupable classes, which can be used multiple times even when they appear in a linear context, but cannot be passed to an unrestricted function. This is necessary to make some API designs work, see the proposal for details.

To me, it seems that this proposal or something like it is necessary to unlock the full potential of linear types. The proposal lays out why monadic API designs don't provide the same benefits, and while there are potential future GHC developments that could make using it even more convenient (existential types, strict let improvements; see proposal), I believe it would already be sufficiently useful with today's GHC to be a valuable addition. Thus, I recommend acceptance.

Please read through the proposal and voice your opinions.

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

Sebastian Graf

17 Feb 17 Feb

3:40 a.m.

New subject: #621: Linear constraints, recommendation: accept

After multiple lengthy discussions that brought forth examples that IMO better motivate the proposal, I retract my earlier vote. However, since there are multiple points of design disagreement between Arnaud and me, I cannot vote in favour of acceptance either and will abstain from voting. Cheers, Sebastian Am Mo., 20. Jan. 2025 um 10:22 Uhr schrieb Sebastian Graf < sgraf1337@gmail.com>:

...

I vote to return the proposal for revision. I listed my feedback in the thread https://github.com/ghc-proposals/ghc-proposals/pull/621#issuecomment-2601848..., but the gist is:

While I am sympathetic to the goal of introducing linearity annotations to

...
constraints, simply because it is a logical extension of -XLinearTypes, I am afraid I do not feel motivated after having considered the examples in the proposal.

In fact, I think the examples overpromise on the utility of linear

...
constraints and the problems it solves have simpler, more direct solutions.

Cheers, Sebastian

Am Di., 14. Jan. 2025 um 23:45 Uhr schrieb Jakob Brünker < jakob.bruenker@gmail.com>:

...
Dear committee,

Arnaud Spiwack and Jack Hughes propose to introduce linear constraints.

These work analogously to linear functions - as can be seen with the new syntax, which is %1 =>, reflecting the existing %1 ->. The motivation is that these constraints make it possible to design linearly typed APIs that are more convenient to use: Without the linear constraints, tokens would have to be passed manually into each function in these cases.

The proposal also introduces dupable classes, which can be used multiple times even when they appear in a linear context, but cannot be passed to an unrestricted function. This is necessary to make some API designs work, see the proposal for details.

To me, it seems that this proposal or something like it is necessary to unlock the full potential of linear types. The proposal lays out why monadic API designs don't provide the same benefits, and while there are potential future GHC developments that could make using it even more convenient (existential types, strict let improvements; see proposal), I believe it would already be sufficiently useful with today's GHC to be a valuable addition. Thus, I recommend acceptance.

Please read through the proposal and voice your opinions.

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

Jakob Brünker

16 Mar 16 Mar

8:41 p.m.

New subject: #621: Linear constraints, recommendation: accept

Hi all, There has been some discussion on the github thread since I presented this to the committee, but it has now quieted down, so it would be great to get some more opinions from you all on this proposal. So far I've only heard from Sebastian. Thanks, Jakob On Mon, Feb 17, 2025 at 9:40 AM Sebastian Graf wrote:

...

After multiple lengthy discussions that brought forth examples that IMO better motivate the proposal, I retract my earlier vote. However, since there are multiple points of design disagreement between Arnaud and me, I cannot vote in favour of acceptance either and will abstain from voting.

Cheers, Sebastian

Am Mo., 20. Jan. 2025 um 10:22 Uhr schrieb Sebastian Graf < sgraf1337@gmail.com>:

...
I vote to return the proposal for revision. I listed my feedback in the thread https://github.com/ghc-proposals/ghc-proposals/pull/621#issuecomment-2601848..., but the gist is:

While I am sympathetic to the goal of introducing linearity annotations

...
to constraints, simply because it is a logical extension of -XLinearTypes, I am afraid I do not feel motivated after having considered the examples in the proposal.

In fact, I think the examples overpromise on the utility of linear

...
constraints and the problems it solves have simpler, more direct solutions.

Cheers, Sebastian

Am Di., 14. Jan. 2025 um 23:45 Uhr schrieb Jakob Brünker < jakob.bruenker@gmail.com>:

...
Dear committee,

Arnaud Spiwack and Jack Hughes propose to introduce linear constraints.

These work analogously to linear functions - as can be seen with the new syntax, which is %1 =>, reflecting the existing %1 ->. The motivation is that these constraints make it possible to design linearly typed APIs that are more convenient to use: Without the linear constraints, tokens would have to be passed manually into each function in these cases.

The proposal also introduces dupable classes, which can be used multiple times even when they appear in a linear context, but cannot be passed to an unrestricted function. This is necessary to make some API designs work, see the proposal for details.

To me, it seems that this proposal or something like it is necessary to unlock the full potential of linear types. The proposal lays out why monadic API designs don't provide the same benefits, and while there are potential future GHC developments that could make using it even more convenient (existential types, strict let improvements; see proposal), I believe it would already be sufficiently useful with today's GHC to be a valuable addition. Thus, I recommend acceptance.

Please read through the proposal and voice your opinions.

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

Simon Peyton Jones

19 Mar 19 Mar

6:16 p.m.

New subject: #621: Linear constraints, recommendation: accept

I had a long conversation with Arnaud about it. I think he is planning revisions Simon On Wed, 19 Mar 2025 at 21:57, Jakob Brünker via ghc-steering-committee < ghc-steering-committee@haskell.org> wrote:

...

Hi all,

There has been some discussion on the github thread since I presented this to the committee, but it has now quieted down, so it would be great to get some more opinions from you all on this proposal. So far I've only heard from Sebastian.

Thanks, Jakob

On Mon, Feb 17, 2025 at 9:40 AM Sebastian Graf wrote:

...
After multiple lengthy discussions that brought forth examples that IMO better motivate the proposal, I retract my earlier vote. However, since there are multiple points of design disagreement between Arnaud and me, I cannot vote in favour of acceptance either and will abstain from voting.

Cheers, Sebastian

Am Mo., 20. Jan. 2025 um 10:22 Uhr schrieb Sebastian Graf < sgraf1337@gmail.com>:

...
I vote to return the proposal for revision. I listed my feedback in the thread https://github.com/ghc-proposals/ghc-proposals/pull/621#issuecomment-2601848..., but the gist is:

While I am sympathetic to the goal of introducing linearity annotations

...
to constraints, simply because it is a logical extension of -XLinearTypes, I am afraid I do not feel motivated after having considered the examples in the proposal.

In fact, I think the examples overpromise on the utility of linear

...
constraints and the problems it solves have simpler, more direct solutions.

Cheers, Sebastian

Am Di., 14. Jan. 2025 um 23:45 Uhr schrieb Jakob Brünker < jakob.bruenker@gmail.com>:

...
Dear committee,

Arnaud Spiwack and Jack Hughes propose to introduce linear constraints.

These work analogously to linear functions - as can be seen with the new syntax, which is %1 =>, reflecting the existing %1 ->. The motivation is that these constraints make it possible to design linearly typed APIs that are more convenient to use: Without the linear constraints, tokens would have to be passed manually into each function in these cases.

The proposal also introduces dupable classes, which can be used multiple times even when they appear in a linear context, but cannot be passed to an unrestricted function. This is necessary to make some API designs work, see the proposal for details.

To me, it seems that this proposal or something like it is necessary to unlock the full potential of linear types. The proposal lays out why monadic API designs don't provide the same benefits, and while there are potential future GHC developments that could make using it even more convenient (existential types, strict let improvements; see proposal), I believe it would already be sufficiently useful with today's GHC to be a valuable addition. Thus, I recommend acceptance.

Please read through the proposal and voice your opinions.

Best, Jakob _______________________________________________ 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

Age (days ago)

126

Last active (days ago)

List overview

Download

4 comments

3 participants

participants (3)

Jakob Brünker
Sebastian Graf
Simon Peyton Jones