Hi committee, Mathieu Boespflug has proposed a new syntax for linear arrows: https://github.com/ghc-proposals/ghc-proposals/pull/356 Currently (from the original linear types proposal), we have #-> to denote a linear function, and # m -> to denote an arbitrary function whose argument has multiplicity m. This proposal suggests three changes: 1. Drop #-> entirely. 2. Use ^ instead of # in the second form, but require that it be a *prefix* usage of ^ (that is, the character after the ^ must not be whitespace). 3. Introduce a new lexeme ^1 that is used to denote linear functions. Alternative: use % in place of ^; % is observed to be more visually apparent in some fonts than ^. In time, the hope is that rule (3) will no longer be needed, if we gain overloaded numbers at the type level (when 1 :: Multiplicity will type-check without a special rule). Motivations for this change come from the experience within Tweag of using linear types. The change away from # also is to avoid a conflict with overloaded labels, once those are allowed in types. The hope is that we can make a decision about this in time for release with GHC 9.0. This proposal is already implemented: https://gitlab.haskell.org/ghc/ghc/-/merge_requests/4020 In conflict with our usual protocol, I will not make a recommendation on this proposal, as I am conflicted with the proposer. However, I do hope that we can come to a conclusion on this quickly, to avoid making a backward-incompatible change after a release. We have four options: A. Keep the syntax as it is. B. Choose to go with ^ C. Choose to go with % D. Choose to go with some other symbol. I don't think there is any particular preference for any one symbol over another. Richard
Hi, I am OK with B or C, with a slight preference with B. I am OK too with moving this proposal fast so it can be reflected on GHC 9.0. Regards, Alejandro El lun., 14 sept. 2020 a las 0:12, Richard Eisenberg (<rae@richarde.dev>) escribió:
Hi committee,
Mathieu Boespflug has proposed a new syntax for linear arrows: https://github.com/ghc-proposals/ghc-proposals/pull/356
Currently (from the original linear types proposal), we have #-> to denote a linear function, and # m -> to denote an arbitrary function whose argument has multiplicity m. This proposal suggests three changes:
1. Drop #-> entirely. 2. Use ^ instead of # in the second form, but require that it be a *prefix* usage of ^ (that is, the character after the ^ must not be whitespace). 3. Introduce a new lexeme ^1 that is used to denote linear functions. Alternative: use % in place of ^; % is observed to be more visually apparent in some fonts than ^.
In time, the hope is that rule (3) will no longer be needed, if we gain overloaded numbers at the type level (when 1 :: Multiplicity will type-check without a special rule).
Motivations for this change come from the experience within Tweag of using linear types. The change away from # also is to avoid a conflict with overloaded labels, once those are allowed in types.
The hope is that we can make a decision about this in time for release with GHC 9.0. This proposal is already implemented: https://gitlab.haskell.org/ghc/ghc/-/merge_requests/4020
In conflict with our usual protocol, I will not make a recommendation on this proposal, as I am conflicted with the proposer. However, I do hope that we can come to a conclusion on this quickly, to avoid making a backward-incompatible change after a release.
We have four options: A. Keep the syntax as it is. B. Choose to go with ^ C. Choose to go with % D. Choose to go with some other symbol. I don't think there is any particular preference for any one symbol over another.
Richard _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
I am supportive. I mildly prefer '%' to '^', purely on grounds of visibility. But I do not feel strongly. Simon | -----Original Message----- | From: ghc-steering-committee <ghc-steering-committee- | bounces@haskell.org> On Behalf Of Richard Eisenberg | Sent: 13 September 2020 23:12 | To: Simon Peyton Jones via ghc-steering-committee <ghc-steering- | committee@haskell.org> | Subject: [ghc-steering-committee] Proposal #356: new syntax for linear | arrows | | Hi committee, | | Mathieu Boespflug has proposed a new syntax for linear arrows: | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithu | b.com%2Fghc-proposals%2Fghc- | proposals%2Fpull%2F356&data=02%7C01%7Csimonpj%40microsoft.com%7C054 | 4526238754e222e3208d85832156e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C | 0%7C637356319418315258&sdata=3266N3ZptTbLQ2EpNgDJh1C1LarPmbUkXAgKcl | 6%2BeE0%3D&reserved=0 | | Currently (from the original linear types proposal), we have #-> to | denote a linear function, and # m -> to denote an arbitrary function | whose argument has multiplicity m. This proposal suggests three | changes: | | 1. Drop #-> entirely. | 2. Use ^ instead of # in the second form, but require that it be a | *prefix* usage of ^ (that is, the character after the ^ must not be | whitespace). | 3. Introduce a new lexeme ^1 that is used to denote linear functions. | Alternative: use % in place of ^; % is observed to be more visually | apparent in some fonts than ^. | | In time, the hope is that rule (3) will no longer be needed, if we gain | overloaded numbers at the type level (when 1 :: Multiplicity will type- | check without a special rule). | | Motivations for this change come from the experience within Tweag of | using linear types. The change away from # also is to avoid a conflict | with overloaded labels, once those are allowed in types. | | The hope is that we can make a decision about this in time for release | with GHC 9.0. This proposal is already implemented: | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitla | b.haskell.org%2Fghc%2Fghc%2F- | %2Fmerge_requests%2F4020&data=02%7C01%7Csimonpj%40microsoft.com%7C0 | 544526238754e222e3208d85832156e%7C72f988bf86f141af91ab2d7cd011db47%7C1% | 7C0%7C637356319418315258&sdata=kp4HBcTvHu6FPAREC4vD3mVfDMbnMztYgW%2 | FPvHTUr0A%3D&reserved=0 | | In conflict with our usual protocol, I will not make a recommendation | on this proposal, as I am conflicted with the proposer. However, I do | hope that we can come to a conclusion on this quickly, to avoid making | a backward-incompatible change after a release. | | We have four options: | A. Keep the syntax as it is. | B. Choose to go with ^ | C. Choose to go with % | D. Choose to go with some other symbol. I don't think there is any | particular preference for any one symbol over another. | | Richard | _______________________________________________ | ghc-steering-committee mailing list | ghc-steering-committee@haskell.org | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail. | haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering- | committee&data=02%7C01%7Csimonpj%40microsoft.com%7C0544526238754e22 | 2e3208d85832156e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637356319 | 418315258&sdata=tkqtcIuFROPvwmEG3gd9zPtcrbhL5cyVN4vNdJqEv1M%3D& | reserved=0
How annoying, how can I now say “I’m trusting the shepherd’s judgement” … ;-) I guess in that case I’ll say I’m trusting Simon PJ, and will go with his vote, as I have no strong opinion of my own. Cheers, Joachim Am Sonntag, den 13.09.2020, 22:12 +0000 schrieb Richard Eisenberg:
Hi committee,
Mathieu Boespflug has proposed a new syntax for linear arrows: https://github.com/ghc-proposals/ghc-proposals/pull/356
Currently (from the original linear types proposal), we have #-> to denote a linear function, and # m -> to denote an arbitrary function whose argument has multiplicity m. This proposal suggests three changes:
1. Drop #-> entirely. 2. Use ^ instead of # in the second form, but require that it be a *prefix* usage of ^ (that is, the character after the ^ must not be whitespace). 3. Introduce a new lexeme ^1 that is used to denote linear functions. Alternative: use % in place of ^; % is observed to be more visually apparent in some fonts than ^.
In time, the hope is that rule (3) will no longer be needed, if we gain overloaded numbers at the type level (when 1 :: Multiplicity will type-check without a special rule).
Motivations for this change come from the experience within Tweag of using linear types. The change away from # also is to avoid a conflict with overloaded labels, once those are allowed in types.
The hope is that we can make a decision about this in time for release with GHC 9.0. This proposal is already implemented: https://gitlab.haskell.org/ghc/ghc/-/merge_requests/4020
In conflict with our usual protocol, I will not make a recommendation on this proposal, as I am conflicted with the proposer. However, I do hope that we can come to a conclusion on this quickly, to avoid making a backward-incompatible change after a release.
We have four options: A. Keep the syntax as it is. B. Choose to go with ^ C. Choose to go with % D. Choose to go with some other symbol. I don't think there is any particular preference for any one symbol over another.
Richard _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/
After looking at the renderings in https://github.com/ghc-proposals/ghc-proposals/pull/356#issuecomment-6902214... , I do prefer `^` over `%`. Not very strongly either. On Mon, Sep 14, 2020 at 6:23 PM Joachim Breitner <mail@joachim-breitner.de> wrote:
How annoying, how can I now say “I’m trusting the shepherd’s judgement” … ;-)
I guess in that case I’ll say I’m trusting Simon PJ, and will go with his vote, as I have no strong opinion of my own.
Cheers, Joachim
Am Sonntag, den 13.09.2020, 22:12 +0000 schrieb Richard Eisenberg:
Hi committee,
Mathieu Boespflug has proposed a new syntax for linear arrows: https://github.com/ghc-proposals/ghc-proposals/pull/356
Currently (from the original linear types proposal), we have #-> to denote a linear function, and # m -> to denote an arbitrary function whose argument has multiplicity m. This proposal suggests three changes:
1. Drop #-> entirely. 2. Use ^ instead of # in the second form, but require that it be a *prefix* usage of ^ (that is, the character after the ^ must not be whitespace). 3. Introduce a new lexeme ^1 that is used to denote linear functions. Alternative: use % in place of ^; % is observed to be more visually apparent in some fonts than ^.
In time, the hope is that rule (3) will no longer be needed, if we gain overloaded numbers at the type level (when 1 :: Multiplicity will type-check without a special rule).
Motivations for this change come from the experience within Tweag of using linear types. The change away from # also is to avoid a conflict with overloaded labels, once those are allowed in types.
The hope is that we can make a decision about this in time for release with GHC 9.0. This proposal is already implemented: https://gitlab.haskell.org/ghc/ghc/-/merge_requests/4020
In conflict with our usual protocol, I will not make a recommendation on this proposal, as I am conflicted with the proposer. However, I do hope that we can come to a conclusion on this quickly, to avoid making a backward-incompatible change after a release.
We have four options: A. Keep the syntax as it is. B. Choose to go with ^ C. Choose to go with % D. Choose to go with some other symbol. I don't think there is any particular preference for any one symbol over another.
Richard _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/
_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
Argh. Of the people who responded, 2 voted for % and 2 voted for ^. No one has voted to reject the proposal. I thus declare the proposal accepted. But with what syntax? I have no conflict with a particular choice of glyph, so I will cast the tie-breaking vote for %. Rationale: ^1 is easy to believe as an exponentiation operator, whereas % has no tradition (within Haskell) as being used as a numerical infix operator. The acceptance of the proposal gets the gears unblocked. If anyone feels this decision premature (or otherwise wrong), please do bleat, as we still have time to change the choice of glyph. Happy Friday, Richard
On Sep 15, 2020, at 2:57 AM, Spiwack, Arnaud <arnaud.spiwack@tweag.io> wrote:
After looking at the renderings in https://github.com/ghc-proposals/ghc-proposals/pull/356#issuecomment-6902214... <https://github.com/ghc-proposals/ghc-proposals/pull/356#issuecomment-690221468> , I do prefer `^` over `%`. Not very strongly either.
On Mon, Sep 14, 2020 at 6:23 PM Joachim Breitner <mail@joachim-breitner.de <mailto:mail@joachim-breitner.de>> wrote: How annoying, how can I now say “I’m trusting the shepherd’s judgement” … ;-)
I guess in that case I’ll say I’m trusting Simon PJ, and will go with his vote, as I have no strong opinion of my own.
Cheers, Joachim
Am Sonntag, den 13.09.2020, 22:12 +0000 schrieb Richard Eisenberg:
Hi committee,
Mathieu Boespflug has proposed a new syntax for linear arrows: https://github.com/ghc-proposals/ghc-proposals/pull/356 <https://github.com/ghc-proposals/ghc-proposals/pull/356>
Currently (from the original linear types proposal), we have #-> to denote a linear function, and # m -> to denote an arbitrary function whose argument has multiplicity m. This proposal suggests three changes:
1. Drop #-> entirely. 2. Use ^ instead of # in the second form, but require that it be a *prefix* usage of ^ (that is, the character after the ^ must not be whitespace). 3. Introduce a new lexeme ^1 that is used to denote linear functions. Alternative: use % in place of ^; % is observed to be more visually apparent in some fonts than ^.
In time, the hope is that rule (3) will no longer be needed, if we gain overloaded numbers at the type level (when 1 :: Multiplicity will type-check without a special rule).
Motivations for this change come from the experience within Tweag of using linear types. The change away from # also is to avoid a conflict with overloaded labels, once those are allowed in types.
The hope is that we can make a decision about this in time for release with GHC 9.0. This proposal is already implemented: https://gitlab.haskell.org/ghc/ghc/-/merge_requests/4020 <https://gitlab.haskell.org/ghc/ghc/-/merge_requests/4020>
In conflict with our usual protocol, I will not make a recommendation on this proposal, as I am conflicted with the proposer. However, I do hope that we can come to a conclusion on this quickly, to avoid making a backward-incompatible change after a release.
We have four options: A. Keep the syntax as it is. B. Choose to go with ^ C. Choose to go with % D. Choose to go with some other symbol. I don't think there is any particular preference for any one symbol over another.
Richard _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org <mailto:ghc-steering-committee@haskell.org> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee <https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee> -- Joachim Breitner mail@joachim-breitner.de <mailto:mail@joachim-breitner.de> http://www.joachim-breitner.de/ <http://www.joachim-breitner.de/>
_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org <mailto:ghc-steering-committee@haskell.org> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee <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
I don't have an opinion on which to use, just FYI in Haskell `%` is used to print and construct Rational numbers. On Fri, Sep 18, 2020 at 11:40 AM Richard Eisenberg <rae@richarde.dev> wrote:
Argh. Of the people who responded, 2 voted for % and 2 voted for ^. No one has voted to reject the proposal.
I thus declare the proposal accepted. But with what syntax? I have no conflict with a particular choice of glyph, so I will cast the tie-breaking vote for %. Rationale: ^1 is easy to believe as an exponentiation operator, whereas % has no tradition (within Haskell) as being used as a numerical infix operator.
The acceptance of the proposal gets the gears unblocked. If anyone feels this decision premature (or otherwise wrong), please do bleat, as we still have time to change the choice of glyph.
Happy Friday, Richard
On Sep 15, 2020, at 2:57 AM, Spiwack, Arnaud <arnaud.spiwack@tweag.io> wrote:
After looking at the renderings in https://github.com/ghc-proposals/ghc-proposals/pull/356#issuecomment-6902214... , I do prefer `^` over `%`. Not very strongly either.
On Mon, Sep 14, 2020 at 6:23 PM Joachim Breitner <mail@joachim-breitner.de> wrote:
How annoying, how can I now say “I’m trusting the shepherd’s judgement” … ;-)
I guess in that case I’ll say I’m trusting Simon PJ, and will go with his vote, as I have no strong opinion of my own.
Cheers, Joachim
Am Sonntag, den 13.09.2020, 22:12 +0000 schrieb Richard Eisenberg:
Hi committee,
Mathieu Boespflug has proposed a new syntax for linear arrows: https://github.com/ghc-proposals/ghc-proposals/pull/356
Currently (from the original linear types proposal), we have #-> to denote a linear function, and # m -> to denote an arbitrary function whose argument has multiplicity m. This proposal suggests three changes:
1. Drop #-> entirely. 2. Use ^ instead of # in the second form, but require that it be a *prefix* usage of ^ (that is, the character after the ^ must not be whitespace). 3. Introduce a new lexeme ^1 that is used to denote linear functions. Alternative: use % in place of ^; % is observed to be more visually apparent in some fonts than ^.
In time, the hope is that rule (3) will no longer be needed, if we gain overloaded numbers at the type level (when 1 :: Multiplicity will type-check without a special rule).
Motivations for this change come from the experience within Tweag of using linear types. The change away from # also is to avoid a conflict with overloaded labels, once those are allowed in types.
The hope is that we can make a decision about this in time for release with GHC 9.0. This proposal is already implemented: https://gitlab.haskell.org/ghc/ghc/-/merge_requests/4020
In conflict with our usual protocol, I will not make a recommendation on this proposal, as I am conflicted with the proposer. However, I do hope that we can come to a conclusion on this quickly, to avoid making a backward-incompatible change after a release.
We have four options: A. Keep the syntax as it is. B. Choose to go with ^ C. Choose to go with % D. Choose to go with some other symbol. I don't think there is any particular preference for any one symbol over another.
Richard _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org
https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/
_______________________________________________ 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
_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
participants (6)
-
Alejandro Serrano Mena -
Iavor Diatchki -
Joachim Breitner -
Richard Eisenberg -
Simon Peyton Jones -
Spiwack, Arnaud