Proposal #274: Quicklook impredicativity, recommendation: accept

Dear all, Last time around that we had a discussion about this proposal, the authors asked to have some more time to revise a few things. Since then, the proposal has been simplified, and the paper accepted (congratulations!). Last time around, those of us who opined were mostly in agreement with accepting the proposal, though there were some distracting complications. Which have since been forked (and accepted) as proposal #287 https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0287-si.... I do believe that this iteration of the proposal is a no-brainer. It simply gives a clear semantics to the unspecified -XImpredicativeTypes. It’s useful, and an implementation already exists (!3220 https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3220). The summary of the proposed specification is: to instantiate a type variable to something of the form forall a. …, go through arguments and look for an absolutely necessary such instantiation (which will happen when there is a data constructor: [a] ~ [forall b.t] iif a = forall b.t). The only point which we may want to discuss is ($), which currently has an ad hoc typing rule baked in the type checker. The proposal suggests removing this baked in rule, and replacing it with making ($) always use the -XImpredicativeTypes typing rule. An alternative, of course, is to simply not treat ($) any specially, and require -XImpredicativeTypes to be explicitly turned on when one wants runST $ do …. But, as the proposal points out, this would break a lot of existing programs. So I agree with the proposal’s choice. In summary, I recommend accepting this proposal in its current state.

I'm in strong support. This will be a nice win for GHC. Richard
On Jun 3, 2020, at 10:03 AM, Spiwack, Arnaud
wrote: Dear all,
Last time around that we had a discussion about this proposal, the authors asked to have some more time to revise a few things. Since then, the proposal has been simplified, and the paper accepted (congratulations!).
Last time around, those of us who opined were mostly in agreement with accepting the proposal, though there were some distracting complications. Which have since been forked (and accepted) as proposal #287 https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0287-si.... I do believe that this iteration of the proposal is a no-brainer. It simply gives a clear semantics to the unspecified -XImpredicativeTypes. It’s useful, and an implementation already exists (!3220 https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3220).
The summary of the proposed specification is: to instantiate a type variable to something of the form forall a. …, go through arguments and look for an absolutely necessary such instantiation (which will happen when there is a data constructor: [a] ~ [forall b.t] iif a = forall b.t).
The only point which we may want to discuss is ($), which currently has an ad hoc typing rule baked in the type checker. The proposal suggests removing this baked in rule, and replacing it with making ($) always use the -XImpredicativeTypes typing rule. An alternative, of course, is to simply not treat ($) any specially, and require -XImpredicativeTypes to be explicitly turned on when one wants runST $ do …. But, as the proposal points out, this would break a lot of existing programs. So I agree with the proposal’s choice.
In summary, I recommend accepting this proposal in its current state.
_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Hi, SGTM. I didn’t actually read the full proposal, but watched Simon PJ’s talk on it. I hope that counts. Cheers, Joachim Am Mittwoch, den 03.06.2020, 11:03 +0200 schrieb Spiwack, Arnaud:
Dear all,
Last time around that we had a discussion about this proposal, the authors asked to have some more time to revise a few things. Since then, the proposal has been simplified, and the paper accepted (congratulations!).
Last time around, those of us who opined were mostly in agreement with accepting the proposal, though there were some distracting complications. Which have since been forked (and accepted) as proposal #287. I do believe that this iteration of the proposal is a no-brainer. It simply gives a clear semantics to the unspecified -XImpredicativeTypes. It’s useful, and an implementation already exists (!3220).
The summary of the proposed specification is: to instantiate a type variable to something of the form forall a. …, go through arguments and look for an absolutely necessary such instantiation (which will happen when there is a data constructor: [a] ~ [forall b.t] iif a = forall b.t).
The only point which we may want to discuss is ($), which currently has an ad hoc typing rule baked in the type checker. The proposal suggests removing this baked in rule, and replacing it with making ($) always use the -XImpredicativeTypes typing rule. An alternative, of course, is to simply not treat ($) any specially, and require -XImpredicativeTypes to be explicitly turned on when one wants runST $ do …. But, as the proposal points out, this would break a lot of existing programs. So I agree with the proposal’s choice.
In summary, I recommend accepting this proposal in its current state.
_______________________________________________ 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/

Hi,
I support the proposal.
Vitaly
ср, 3 июн. 2020 г. в 12:04, Spiwack, Arnaud
Dear all,
Last time around that we had a discussion about this proposal, the authors asked to have some more time to revise a few things. Since then, the proposal has been simplified, and the paper accepted (congratulations!).
Last time around, those of us who opined were mostly in agreement with accepting the proposal, though there were some distracting complications. Which have since been forked (and accepted) as proposal #287 https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0287-si.... I do believe that this iteration of the proposal is a no-brainer. It simply gives a clear semantics to the unspecified -XImpredicativeTypes. It’s useful, and an implementation already exists (!3220 https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3220).
The summary of the proposed specification is: to instantiate a type variable to something of the form forall a. …, go through arguments and look for an absolutely necessary such instantiation (which will happen when there is a data constructor: [a] ~ [forall b.t] iif a = forall b.t).
The only point which we may want to discuss is ($), which currently has an ad hoc typing rule baked in the type checker. The proposal suggests removing this baked in rule, and replacing it with making ($) always use the -XImpredicativeTypes typing rule. An alternative, of course, is to simply not treat ($) any specially, and require -XImpredicativeTypes to be explicitly turned on when one wants runST $ do …. But, as the proposal points out, this would break a lot of existing programs. So I agree with the proposal’s choice.
In summary, I recommend accepting this proposal in its current state. _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Dear all, I didn't give ourselves a deadline on this one. Let me fix this: unless a significant objection has arisen by 12th June, let us accept this proposal. Best, Arnaud

Dear all,
If you want to voice an opinion on this proposal, don't forget to do so
before Friday night (12th June, anywhere on Earth). After that, I'll
consider silence as assent and accept the proposal.
Best,
Arnaud
On Thu, Jun 4, 2020 at 7:58 AM Spiwack, Arnaud
Dear all,
I didn't give ourselves a deadline on this one. Let me fix this: unless a significant objection has arisen by 12th June, let us accept this proposal.
Best, Arnaud

Dear all,
I don't know whether to take the lack of response as a good thing (as in:
it's so uncontroversial that nobody has anything to say about it). But I
believe it is time to accept this proposal.
Simon, Alejandro: I've made a couple of typo-level suggestions in the
proposal, have a look at them before we merge.
Joachim: I have marked the proposal as accepted, but I forgot the process
after that, again. Who is in charge of merging?
On Wed, Jun 10, 2020 at 11:33 AM Spiwack, Arnaud
Dear all,
If you want to voice an opinion on this proposal, don't forget to do so before Friday night (12th June, anywhere on Earth). After that, I'll consider silence as assent and accept the proposal.
Best, Arnaud
On Thu, Jun 4, 2020 at 7:58 AM Spiwack, Arnaud
wrote: Dear all,
I didn't give ourselves a deadline on this one. Let me fix this: unless a significant objection has arisen by 12th June, let us accept this proposal.
Best, Arnaud

Hi, Am Montag, den 15.06.2020, 09:52 +0200 schrieb Spiwack, Arnaud:
Joachim: I have marked the proposal as accepted, but I forgot the process after that, again. Who is in charge of merging?
I’ll take care of it. Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/
participants (4)
-
Joachim Breitner
-
Richard Eisenberg
-
Spiwack, Arnaud
-
Vitaly Bragilevsky