#287: Simplify subsumption , recommendation: accept
Dear all, As the shepherd for proposal #287 [ https://github.com/ghc-proposals/ghc-proposals/pull/287 ], I recommend acceptance Summary The proposal is to remove a bunch of typing rules meant to make RankNTypes a bit more powerful (covariance and contravariance of the arrow constructor, as well as deep instantiation and deep skolemisation). The problem with these rules is that 1/ they complicate the type checker 2/ They are implemented by performing eta-expansion during elaboration, which changes the semantics of program 3/ Dropping (some of) them is beneficial for the quick-look story (proposal currently on hold). The authors have tried this change on all of Stackage, and could come up with simple fixes (~300 lines of which) for all but 2 packages (namely, singleton, because of template haskell stuff, and labels for reason not well identified). Rationale The common point of all these features is that they jiggle the position of foralls around. Which sounds reasonable at first glance. But really, they tend to interact badly with other stuff (I don't remember the circumstances, but there was a discussion of deep instantiation and deep skolemisation in the context of linear types as well). Basically, they are rather fragile features, I'd rather we did without them. I think that 300 lines of simple fixes for all of Stackage is a very small number. So it is legitimate to consider this change to have low impact. Regarding the singleton, I'm sure Richard will be happy to fix it ;-) . Only labels remains. It shouldn't be a blocker. Remaining question There is one open question on the pull request thread. Namely, how to schedule the removal. Two paths are being discussed 1. Add a `-XLessSubsumption` flag, turn it off by default, then turn it on by default in version n+1, then remove the subsumption rules altogether in version n+3 2. Simply remove the code, preferably early in the release cycle, communicate profusely. The thread participants seem to lean towards (2). The reason being that this is a change where it is easy to write code compatible with previous versions of the compiler (everything which compiles after this change also compiles before this change). Also, there is a preference for removing the relevant code sooner rather than later. But I'd like the opinion of the committee. Best, Arnaud
I support acceptance as well. Changing the semantics of the program as part of type-checking is just bizarre and it seems like the impact in terms of required code changes is quite limited. Given how easy the fixes appear to be, and the fact that the fixed program will compile just fine with older GHCs, I'm inclined to support option (2): ripping the code out immediately. I've left a comment on the PR asking if we can do so while providing helpful fixit hints to unaware users. On Fri, Jan 17, 2020, at 08:49, Spiwack, Arnaud wrote:
Dear all,
As the shepherd for proposal #287 [ https://github.com/ghc-proposals/ghc-proposals/pull/287 ], I recommend acceptance
Summary
The proposal is to remove a bunch of typing rules meant to make RankNTypes a bit more powerful (covariance and contravariance of the arrow constructor, as well as deep instantiation and deep skolemisation). The problem with these rules is that 1/ they complicate the type checker 2/ They are implemented by performing eta-expansion during elaboration, which changes the semantics of program 3/ Dropping (some of) them is beneficial for the quick-look story (proposal currently on hold).
The authors have tried this change on all of Stackage, and could come up with simple fixes (~300 lines of which) for all but 2 packages (namely, singleton, because of template haskell stuff, and labels for reason not well identified).
Rationale
The common point of all these features is that they jiggle the position of foralls around. Which sounds reasonable at first glance. But really, they tend to interact badly with other stuff (I don't remember the circumstances, but there was a discussion of deep instantiation and deep skolemisation in the context of linear types as well). Basically, they are rather fragile features, I'd rather we did without them.
I think that 300 lines of simple fixes for all of Stackage is a very small number. So it is legitimate to consider this change to have low impact. Regarding the singleton, I'm sure Richard will be happy to fix it ;-) . Only labels remains. It shouldn't be a blocker.
Remaining question
There is one open question on the pull request thread. Namely, how to schedule the removal. Two paths are being discussed 1. Add a `-XLessSubsumption` flag, turn it off by default, then turn it on by default in version n+1, then remove the subsumption rules altogether in version n+3 2. Simply remove the code, preferably early in the release cycle, communicate profusely. The thread participants seem to lean towards (2). The reason being that this is a change where it is easy to write code compatible with previous versions of the compiler (everything which compiles after this change also compiles before this change). Also, there is a preference for removing the relevant code sooner rather than later. But I'd like the opinion of the committee.
Best, Arnaud _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
I'm in support of acceptance and the quick transition strategy. One more bit of rationale: if we didn't have these features and someone proposed them today, we'd shoot them down without much discussion, given the way these features invisibly change the semantics of programs. Richard
On Jan 17, 2020, at 2:16 PM, Eric Seidel <eric@seidel.io> wrote:
I support acceptance as well. Changing the semantics of the program as part of type-checking is just bizarre and it seems like the impact in terms of required code changes is quite limited.
Given how easy the fixes appear to be, and the fact that the fixed program will compile just fine with older GHCs, I'm inclined to support option (2): ripping the code out immediately. I've left a comment on the PR asking if we can do so while providing helpful fixit hints to unaware users.
On Fri, Jan 17, 2020, at 08:49, Spiwack, Arnaud wrote:
Dear all,
As the shepherd for proposal #287 [ https://github.com/ghc-proposals/ghc-proposals/pull/287 ], I recommend acceptance
Summary
The proposal is to remove a bunch of typing rules meant to make RankNTypes a bit more powerful (covariance and contravariance of the arrow constructor, as well as deep instantiation and deep skolemisation). The problem with these rules is that 1/ they complicate the type checker 2/ They are implemented by performing eta-expansion during elaboration, which changes the semantics of program 3/ Dropping (some of) them is beneficial for the quick-look story (proposal currently on hold).
The authors have tried this change on all of Stackage, and could come up with simple fixes (~300 lines of which) for all but 2 packages (namely, singleton, because of template haskell stuff, and labels for reason not well identified).
Rationale
The common point of all these features is that they jiggle the position of foralls around. Which sounds reasonable at first glance. But really, they tend to interact badly with other stuff (I don't remember the circumstances, but there was a discussion of deep instantiation and deep skolemisation in the context of linear types as well). Basically, they are rather fragile features, I'd rather we did without them.
I think that 300 lines of simple fixes for all of Stackage is a very small number. So it is legitimate to consider this change to have low impact. Regarding the singleton, I'm sure Richard will be happy to fix it ;-) . Only labels remains. It shouldn't be a blocker.
Remaining question
There is one open question on the pull request thread. Namely, how to schedule the removal. Two paths are being discussed 1. Add a `-XLessSubsumption` flag, turn it off by default, then turn it on by default in version n+1, then remove the subsumption rules altogether in version n+3 2. Simply remove the code, preferably early in the release cycle, communicate profusely. The thread participants seem to lean towards (2). The reason being that this is a change where it is easy to write code compatible with previous versions of the compiler (everything which compiles after this change also compiles before this change). Also, there is a preference for removing the relevant code sooner rather than later. But I'd like the opinion of the committee.
Best, Arnaud _______________________________________________ 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 <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>
Hi, I’m with Eric here. Cheers, Joachim Am Freitag, den 17.01.2020, 09:16 -0500 schrieb Eric Seidel:
I support acceptance as well. Changing the semantics of the program as part of type-checking is just bizarre and it seems like the impact in terms of required code changes is quite limited.
Given how easy the fixes appear to be, and the fact that the fixed program will compile just fine with older GHCs, I'm inclined to support option (2): ripping the code out immediately. I've left a comment on the PR asking if we can do so while providing helpful fixit hints to unaware users.
On Fri, Jan 17, 2020, at 08:49, Spiwack, Arnaud wrote:
Dear all,
As the shepherd for proposal #287 [ https://github.com/ghc-proposals/ghc-proposals/pull/287 ], I recommend acceptance
Summary
The proposal is to remove a bunch of typing rules meant to make RankNTypes a bit more powerful (covariance and contravariance of the arrow constructor, as well as deep instantiation and deep skolemisation). The problem with these rules is that 1/ they complicate the type checker 2/ They are implemented by performing eta-expansion during elaboration, which changes the semantics of program 3/ Dropping (some of) them is beneficial for the quick-look story (proposal currently on hold).
The authors have tried this change on all of Stackage, and could come up with simple fixes (~300 lines of which) for all but 2 packages (namely, singleton, because of template haskell stuff, and labels for reason not well identified).
Rationale
The common point of all these features is that they jiggle the position of foralls around. Which sounds reasonable at first glance. But really, they tend to interact badly with other stuff (I don't remember the circumstances, but there was a discussion of deep instantiation and deep skolemisation in the context of linear types as well). Basically, they are rather fragile features, I'd rather we did without them.
I think that 300 lines of simple fixes for all of Stackage is a very small number. So it is legitimate to consider this change to have low impact. Regarding the singleton, I'm sure Richard will be happy to fix it ;-) . Only labels remains. It shouldn't be a blocker.
Remaining question
There is one open question on the pull request thread. Namely, how to schedule the removal. Two paths are being discussed 1. Add a `-XLessSubsumption` flag, turn it off by default, then turn it on by default in version n+1, then remove the subsumption rules altogether in version n+3 2. Simply remove the code, preferably early in the release cycle, communicate profusely. The thread participants seem to lean towards (2). The reason being that this is a change where it is easy to write code compatible with previous versions of the compiler (everything which compiles after this change also compiles before this change). Also, there is a preference for removing the relevant code sooner rather than later. But I'd like the opinion of the committee.
Best, Arnaud _______________________________________________ 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 -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/
I'm next to support the acceptance with the quick transition strategy. Vitaly пт, 17 янв. 2020 г. в 16:50, Spiwack, Arnaud <arnaud.spiwack@tweag.io>:
Dear all,
As the shepherd for proposal #287 [ https://github.com/ghc-proposals/ghc-proposals/pull/287 ], I recommend acceptance
Summary
The proposal is to remove a bunch of typing rules meant to make RankNTypes a bit more powerful (covariance and contravariance of the arrow constructor, as well as deep instantiation and deep skolemisation). The problem with these rules is that 1/ they complicate the type checker 2/ They are implemented by performing eta-expansion during elaboration, which changes the semantics of program 3/ Dropping (some of) them is beneficial for the quick-look story (proposal currently on hold).
The authors have tried this change on all of Stackage, and could come up with simple fixes (~300 lines of which) for all but 2 packages (namely, singleton, because of template haskell stuff, and labels for reason not well identified).
Rationale
The common point of all these features is that they jiggle the position of foralls around. Which sounds reasonable at first glance. But really, they tend to interact badly with other stuff (I don't remember the circumstances, but there was a discussion of deep instantiation and deep skolemisation in the context of linear types as well). Basically, they are rather fragile features, I'd rather we did without them.
I think that 300 lines of simple fixes for all of Stackage is a very small number. So it is legitimate to consider this change to have low impact. Regarding the singleton, I'm sure Richard will be happy to fix it ;-) . Only labels remains. It shouldn't be a blocker.
Remaining question
There is one open question on the pull request thread. Namely, how to schedule the removal. Two paths are being discussed
1. Add a `-XLessSubsumption` flag, turn it off by default, then turn it on by default in version n+1, then remove the subsumption rules altogether in version n+3 2. Simply remove the code, preferably early in the release cycle, communicate profusely.
The thread participants seem to lean towards (2). The reason being that this is a change where it is easy to write code compatible with previous versions of the compiler (everything which compiles after this change also compiles before this change). Also, there is a preference for removing the relevant code sooner rather than later. But I'd like the opinion of the committee.
Best, Arnaud _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
I am in support On Fri, Jan 17, 2020, 05:50 Spiwack, Arnaud <arnaud.spiwack@tweag.io> wrote:
Dear all,
As the shepherd for proposal #287 [ https://github.com/ghc-proposals/ghc-proposals/pull/287 ], I recommend acceptance
Summary
The proposal is to remove a bunch of typing rules meant to make RankNTypes a bit more powerful (covariance and contravariance of the arrow constructor, as well as deep instantiation and deep skolemisation). The problem with these rules is that 1/ they complicate the type checker 2/ They are implemented by performing eta-expansion during elaboration, which changes the semantics of program 3/ Dropping (some of) them is beneficial for the quick-look story (proposal currently on hold).
The authors have tried this change on all of Stackage, and could come up with simple fixes (~300 lines of which) for all but 2 packages (namely, singleton, because of template haskell stuff, and labels for reason not well identified).
Rationale
The common point of all these features is that they jiggle the position of foralls around. Which sounds reasonable at first glance. But really, they tend to interact badly with other stuff (I don't remember the circumstances, but there was a discussion of deep instantiation and deep skolemisation in the context of linear types as well). Basically, they are rather fragile features, I'd rather we did without them.
I think that 300 lines of simple fixes for all of Stackage is a very small number. So it is legitimate to consider this change to have low impact. Regarding the singleton, I'm sure Richard will be happy to fix it ;-) . Only labels remains. It shouldn't be a blocker.
Remaining question
There is one open question on the pull request thread. Namely, how to schedule the removal. Two paths are being discussed
1. Add a `-XLessSubsumption` flag, turn it off by default, then turn it on by default in version n+1, then remove the subsumption rules altogether in version n+3 2. Simply remove the code, preferably early in the release cycle, communicate profusely.
The thread participants seem to lean towards (2). The reason being that this is a change where it is easy to write code compatible with previous versions of the compiler (everything which compiles after this change also compiles before this change). Also, there is a preference for removing the relevant code sooner rather than later. But I'd like the opinion of the committee.
Best, Arnaud _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
Support seems unanimous so far. Barring any counter-argument by then, I'll mark the proposal as accepted, with the short path, on Thursday. /Arnaud On Mon, Jan 20, 2020 at 7:08 PM Iavor Diatchki <iavor.diatchki@gmail.com> wrote:
I am in support
On Fri, Jan 17, 2020, 05:50 Spiwack, Arnaud <arnaud.spiwack@tweag.io> wrote:
Dear all,
As the shepherd for proposal #287 [ https://github.com/ghc-proposals/ghc-proposals/pull/287 ], I recommend acceptance
Summary
The proposal is to remove a bunch of typing rules meant to make RankNTypes a bit more powerful (covariance and contravariance of the arrow constructor, as well as deep instantiation and deep skolemisation). The problem with these rules is that 1/ they complicate the type checker 2/ They are implemented by performing eta-expansion during elaboration, which changes the semantics of program 3/ Dropping (some of) them is beneficial for the quick-look story (proposal currently on hold).
The authors have tried this change on all of Stackage, and could come up with simple fixes (~300 lines of which) for all but 2 packages (namely, singleton, because of template haskell stuff, and labels for reason not well identified).
Rationale
The common point of all these features is that they jiggle the position of foralls around. Which sounds reasonable at first glance. But really, they tend to interact badly with other stuff (I don't remember the circumstances, but there was a discussion of deep instantiation and deep skolemisation in the context of linear types as well). Basically, they are rather fragile features, I'd rather we did without them.
I think that 300 lines of simple fixes for all of Stackage is a very small number. So it is legitimate to consider this change to have low impact. Regarding the singleton, I'm sure Richard will be happy to fix it ;-) . Only labels remains. It shouldn't be a blocker.
Remaining question
There is one open question on the pull request thread. Namely, how to schedule the removal. Two paths are being discussed
1. Add a `-XLessSubsumption` flag, turn it off by default, then turn it on by default in version n+1, then remove the subsumption rules altogether in version n+3 2. Simply remove the code, preferably early in the release cycle, communicate profusely.
The thread participants seem to lean towards (2). The reason being that this is a change where it is easy to write code compatible with previous versions of the compiler (everything which compiles after this change also compiles before this change). Also, there is a preference for removing the relevant code sooner rather than later. But I'd like the opinion of the committee.
Best, Arnaud _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
I've now marked the proposal as accepted. On Tue, Jan 21, 2020 at 8:43 AM Spiwack, Arnaud <arnaud.spiwack@tweag.io> wrote:
Support seems unanimous so far. Barring any counter-argument by then, I'll mark the proposal as accepted, with the short path, on Thursday.
/Arnaud
On Mon, Jan 20, 2020 at 7:08 PM Iavor Diatchki <iavor.diatchki@gmail.com> wrote:
I am in support
On Fri, Jan 17, 2020, 05:50 Spiwack, Arnaud <arnaud.spiwack@tweag.io> wrote:
Dear all,
As the shepherd for proposal #287 [ https://github.com/ghc-proposals/ghc-proposals/pull/287 ], I recommend acceptance
Summary
The proposal is to remove a bunch of typing rules meant to make RankNTypes a bit more powerful (covariance and contravariance of the arrow constructor, as well as deep instantiation and deep skolemisation). The problem with these rules is that 1/ they complicate the type checker 2/ They are implemented by performing eta-expansion during elaboration, which changes the semantics of program 3/ Dropping (some of) them is beneficial for the quick-look story (proposal currently on hold).
The authors have tried this change on all of Stackage, and could come up with simple fixes (~300 lines of which) for all but 2 packages (namely, singleton, because of template haskell stuff, and labels for reason not well identified).
Rationale
The common point of all these features is that they jiggle the position of foralls around. Which sounds reasonable at first glance. But really, they tend to interact badly with other stuff (I don't remember the circumstances, but there was a discussion of deep instantiation and deep skolemisation in the context of linear types as well). Basically, they are rather fragile features, I'd rather we did without them.
I think that 300 lines of simple fixes for all of Stackage is a very small number. So it is legitimate to consider this change to have low impact. Regarding the singleton, I'm sure Richard will be happy to fix it ;-) . Only labels remains. It shouldn't be a blocker.
Remaining question
There is one open question on the pull request thread. Namely, how to schedule the removal. Two paths are being discussed
1. Add a `-XLessSubsumption` flag, turn it off by default, then turn it on by default in version n+1, then remove the subsumption rules altogether in version n+3 2. Simply remove the code, preferably early in the release cycle, communicate profusely.
The thread participants seem to lean towards (2). The reason being that this is a change where it is easy to write code compatible with previous versions of the compiler (everything which compiles after this change also compiles before this change). Also, there is a preference for removing the relevant code sooner rather than later. But I'd like the opinion of the committee.
Best, Arnaud _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
participants (6)
-
Eric Seidel -
Iavor Diatchki -
Joachim Breitner -
Richard Eisenberg -
Spiwack, Arnaud -
Vitaly Bragilevsky