Re: Is simplified subsumption really necessary?
Somewhat related: while migrating quite a bit of code to GHC > 9 I found that after seeing some errors it was quite easy to identify (from error messages) when I needed to manually eta-expand something. I'm wondering if the error messages could be better (explicitly mentioning simplified subsumption and eta-expanding as a solution) or perhaps if the migration could even have been automated? The ship might have sailed on this too, but perhaps something to keep in mind for future changes. Adam Sandberg Eriksson On Sun, 20 Jun 2021, at 23:22, Simon Peyton Jones via ghc-devs wrote: > Yes, maybe the seq thing would be possible. But it feels like a hack, and > I’m far from convinced that the optimiser would really eliminate the > overhead.If I was convinced that deep subsumption was really better, it > might be worth investigating the hack more deeply. But in fact I’ve become > convinced of the opposite, that deep subsumption just isn’t worth the extra > complexity – the simpler system allows Quick Look for example. > > Simon > > *From:* John Ericson > *Sent:* 20 June 2021 18:07 > *To:* ghc-devs ; Simon Peyton Jones > > *Subject:* Re: Is simplified subsumption really necessary? > > I'm sorry, I misunderstood the paper and thought the depth of the > instantiation and subsumption could be varied more independently. > > That said, what about the seq example below? Does forcing any function that > is eta expanded like that sketchy to you? There is still a runtime cost to > the eta expansion, but think with more elbow grease that could also be > addressed (post-type-erasure optimization or new coercions). > > John > > On 6/18/21 3:56 PM, Simon Peyton Jones wrote: >> Richard’s paper argues for lazy rather than eager instantiation. >> >> It does *not* argue for deep rather than shallow subsumption and >> instantiation; on the contrary, it argues for shallow. (That is, for >> “simple subsumption”.) And it is simple subsumption that is the focus of >> this conversation. >> >> Simon >> >> *From:* John Ericson >> *Sent:* 18 June 2021 16:56 >> *To:* ghc-devs >> *Cc:* Simon Peyton Jones >> *Subject:* Re: Is simplified subsumption really necessary? >> >> On 6/16/21 12:00 PM, Simon Peyton Jones via ghc-devs wrote: >> >>> I’m sorry to hear that Chris. It’s exactly backwards from what I would >>> expect – the typing rules with simple subsumption are, well, simpler than >>> those for complicated subsumption, and so one might hope that your >>> intuition had fewer complexities to grapple with. >> In https://richarde.dev/papers/2021/stability/stability.pdf >> <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fricharde.dev%2Fpapers%2F2021%2Fstability%2Fstability.pdf=04%7C01%7Csimonpj%40microsoft.com%7Cb9916cabe3744e44375008d9340dca51%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637598056497592691%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000=SqgQIEVpLIARanGOqvKDNOjG%2FtLFZ6v1XVXzCFD1FQE%3D=0> >> it is written >> >>> The analysis around stability in this paper strongly suggests that GHC >>> should use the lazy, shallow approach to instantiation. Yet the struggles >>> with lazy instantiation above remain. In order to simplify the >>> implementation, GHC has recently (for GHC 9.0) switched to use exclusively >>> eager instantiation.This choice sacrifices stability for convenience in >>> implementation. >>> >> I think the principles outlined in the paper are very good, and explain the >> queasiness some users may feel in 9.0 >> >>> >>> But wouldn't it be possible to choose a desugaring with seq that doesn't do >>> so? >>> >>> I just don’t know how to do that. Maybe someone else does. >> Is it not >> >> f `seq` \x -> f x >> >> and similar? I haven't thought about the issue in a while or in very much >> depth, but when I first discussed the proposal years back with some other >> people at work, they spit-balled the same counter-proposal. >> >> >> >> Having little "skin in the game" as I haven't yet ported any serious >> programs over to 9.0, I suppose I am glad the experimentation with QuickLook >> is happening, and OK that our accepting on-par fewer programs now opens >> design space for later (i.e. we got the breakage out of the way.) But I >> certainly think there are improvements in the spirit outlined in Richard's >> paper to be done down the road. >> >> John >> > ___ > ghc-devs mailing list > ghc-devs@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
RE: Is simplified subsumption really necessary?
Yes, maybe the seq thing would be possible. But it feels like a hack, and I'm far from convinced that the optimiser would really eliminate the overhead. If I was convinced that deep subsumption was really better, it might be worth investigating the hack more deeply. But in fact I've become convinced of the opposite, that deep subsumption just isn't worth the extra complexity - the simpler system allows Quick Look for example. Simon From: John Ericson Sent: 20 June 2021 18:07 To: ghc-devs ; Simon Peyton Jones Subject: Re: Is simplified subsumption really necessary? I'm sorry, I misunderstood the paper and thought the depth of the instantiation and subsumption could be varied more independently. That said, what about the seq example below? Does forcing any function that is eta expanded like that sketchy to you? There is still a runtime cost to the eta expansion, but think with more elbow grease that could also be addressed (post-type-erasure optimization or new coercions). John On 6/18/21 3:56 PM, Simon Peyton Jones wrote: Richard's paper argues for lazy rather than eager instantiation. It does not argue for deep rather than shallow subsumption and instantiation; on the contrary, it argues for shallow. (That is, for "simple subsumption".) And it is simple subsumption that is the focus of this conversation. Simon From: John Ericson <mailto:john.ericson@obsidian.systems> Sent: 18 June 2021 16:56 To: ghc-devs <mailto:ghc-devs@haskell.org> Cc: Simon Peyton Jones <mailto:simo...@microsoft.com> Subject: Re: Is simplified subsumption really necessary? On 6/16/21 12:00 PM, Simon Peyton Jones via ghc-devs wrote: I'm sorry to hear that Chris. It's exactly backwards from what I would expect - the typing rules with simple subsumption are, well, simpler than those for complicated subsumption, and so one might hope that your intuition had fewer complexities to grapple with. In https://richarde.dev/papers/2021/stability/stability.pdf<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fricharde.dev%2Fpapers%2F2021%2Fstability%2Fstability.pdf=04%7C01%7Csimonpj%40microsoft.com%7Cb9916cabe3744e44375008d9340dca51%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637598056497592691%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000=SqgQIEVpLIARanGOqvKDNOjG%2FtLFZ6v1XVXzCFD1FQE%3D=0> it is written The analysis around stability in this paper strongly suggests that GHC should use the lazy, shallow approach to instantiation. Yet the struggles with lazy instantiation above remain. In order to simplify the implementation, GHC has recently (for GHC 9.0) switched to use exclusively eager instantiation.This choice sacrifices stability for convenience in implementation. I think the principles outlined in the paper are very good, and explain the queasiness some users may feel in 9.0 But wouldn't it be possible to choose a desugaring with seq that doesn't do so? I just don't know how to do that. Maybe someone else does. Is it not f `seq` \x -> f x and similar? I haven't thought about the issue in a while or in very much depth, but when I first discussed the proposal years back with some other people at work, they spit-balled the same counter-proposal. Having little "skin in the game" as I haven't yet ported any serious programs over to 9.0, I suppose I am glad the experimentation with QuickLook is happening, and OK that our accepting on-par fewer programs now opens design space for later (i.e. we got the breakage out of the way.) But I certainly think there are improvements in the spirit outlined in Richard's paper to be done down the road. John ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: Is simplified subsumption really necessary?
I'm sorry, I misunderstood the paper and thought the depth of the instantiation and subsumption could be varied more independently. That said, what about the seq example below? Does forcing any function that is eta expanded like that sketchy to you? There is still a runtime cost to the eta expansion, but think with more elbow grease that could also be addressed (post-type-erasure optimization or new coercions). John On 6/18/21 3:56 PM, Simon Peyton Jones wrote: Richard’s paper argues for lazy rather than eager instantiation. It does *not* argue for deep rather than shallow subsumption and instantiation; on the contrary, it argues for shallow. (That is, for “simple subsumption”.) And it is simple subsumption that is the focus of this conversation. Simon *From:*John Ericson *Sent:* 18 June 2021 16:56 *To:* ghc-devs *Cc:* Simon Peyton Jones *Subject:* Re: Is simplified subsumption really necessary? On 6/16/21 12:00 PM, Simon Peyton Jones via ghc-devs wrote: I’m sorry to hear that Chris. It’s exactly backwards from what I would expect – the typing rules with simple subsumption are, well, simpler than those for complicated subsumption, and so one might hope that your intuition had fewer complexities to grapple with. In https://richarde.dev/papers/2021/stability/stability.pdf <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fricharde.dev%2Fpapers%2F2021%2Fstability%2Fstability.pdf=04%7C01%7Csimonpj%40microsoft.com%7C7655b09d06a54a4af03508d9327193cd%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637596286139778988%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000=R1quXKjsnEjusvX%2BSxhPT25t%2B%2Bwqwo7mTPhnulvctQ0%3D=0> it is written The analysis around stability in this paper strongly suggests that GHC should use the lazy, shallow approach to instantiation. Yet the struggles with lazy instantiation above remain. In order to simplify the implementation, GHC has recently (for GHC 9.0) switched to use exclusively eager instantiation.This choice sacrifices stability for convenience in implementation. I think the principles outlined in the paper are very good, and explain the queasiness some users may feel in 9.0 But wouldn't it be possible to choose a desugaring with seq that doesn't do so? I just don’t know how to do that. Maybe someone else does. Is it not f `seq` \x -> f x and similar? I haven't thought about the issue in a while or in very much depth, but when I first discussed the proposal years back with some other people at work, they spit-balled the same counter-proposal. Having little "skin in the game" as I haven't yet ported any serious programs over to 9.0, I suppose I am glad the experimentation with QuickLook is happening, and OK that our accepting on-par fewer programs now opens design space for later (i.e. we got the breakage out of the way.) But I certainly think there are improvements in the spirit outlined in Richard's paper to be done down the road. John ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
RE: Is simplified subsumption really necessary?
Richard's paper argues for lazy rather than eager instantiation. It does not argue for deep rather than shallow subsumption and instantiation; on the contrary, it argues for shallow. (That is, for "simple subsumption".) And it is simple subsumption that is the focus of this conversation. Simon From: John Ericson Sent: 18 June 2021 16:56 To: ghc-devs Cc: Simon Peyton Jones Subject: Re: Is simplified subsumption really necessary? On 6/16/21 12:00 PM, Simon Peyton Jones via ghc-devs wrote: I'm sorry to hear that Chris. It's exactly backwards from what I would expect - the typing rules with simple subsumption are, well, simpler than those for complicated subsumption, and so one might hope that your intuition had fewer complexities to grapple with. In https://richarde.dev/papers/2021/stability/stability.pdf<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fricharde.dev%2Fpapers%2F2021%2Fstability%2Fstability.pdf=04%7C01%7Csimonpj%40microsoft.com%7C7655b09d06a54a4af03508d9327193cd%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637596286139778988%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000=R1quXKjsnEjusvX%2BSxhPT25t%2B%2Bwqwo7mTPhnulvctQ0%3D=0> it is written The analysis around stability in this paper strongly suggests that GHC should use the lazy, shallow approach to instantiation. Yet the struggles with lazy instantiation above remain. In order to simplify the implementation, GHC has recently (for GHC 9.0) switched to use exclusively eager instantiation.This choice sacrifices stability for convenience in implementation. I think the principles outlined in the paper are very good, and explain the queasiness some users may feel in 9.0 But wouldn't it be possible to choose a desugaring with seq that doesn't do so? I just don't know how to do that. Maybe someone else does. Is it not f `seq` \x -> f x and similar? I haven't thought about the issue in a while or in very much depth, but when I first discussed the proposal years back with some other people at work, they spit-balled the same counter-proposal. Having little "skin in the game" as I haven't yet ported any serious programs over to 9.0, I suppose I am glad the experimentation with QuickLook is happening, and OK that our accepting on-par fewer programs now opens design space for later (i.e. we got the breakage out of the way.) But I certainly think there are improvements in the spirit outlined in Richard's paper to be done down the road. John ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: Is simplified subsumption really necessary?
On 6/16/21 12:00 PM, Simon Peyton Jones via ghc-devs wrote: I’m sorry to hear that Chris. It’s exactly backwards from what I would expect – the typing rules with simple subsumption are, well, simpler than those for complicated subsumption, and so one might hope that your intuition had fewer complexities to grapple with. In https://richarde.dev/papers/2021/stability/stability.pdf it is written The analysis around stability in this paper strongly suggests that GHC should use the lazy, shallow approach to instantiation. Yet the struggles with lazy instantiation above remain. In order to simplify the implementation, GHC has recently (for GHC 9.0) switched to use exclusively eager instantiation.This choice sacrifices stability for convenience in implementation. I think the principles outlined in the paper are very good, and explain the queasiness some users may feel in 9.0 But wouldn't it be possible to choose a desugaring with seq that doesn't do so? I just don’t know how to do that. Maybe someone else does. Is it not f `seq` \x -> f x and similar? I haven't thought about the issue in a while or in very much depth, but when I first discussed the proposal years back with some other people at work, they spit-balled the same counter-proposal. Having little "skin in the game" as I haven't yet ported any serious programs over to 9.0, I suppose I am glad the experimentation with QuickLook is happening, and OK that our accepting on-par fewer programs now opens design space for later (i.e. we got the breakage out of the way.) But I certainly think there are improvements in the spirit outlined in Richard's paper to be done down the road. John ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
RE: Is simplified subsumption really necessary?
rather, it's that it completely screws up my intuition about what should be valid Haskell. I'm sorry to hear that Chris. It's exactly backwards from what I would expect - the typing rules with simple subsumption are, well, simpler than those for complicated subsumption, and so one might hope that your intuition had fewer complexities to grapple with. Maybe it's partly a matter of explanation and presentation. Do you have an example of a case in which your intuition was screwed up by the simple subsumption rules? Discussing in the abstract is often un-illuminating. But wouldn't it be possible to choose a desugaring with seq that doesn't do so? I just don't know how to do that. Maybe someone else does. Meanwhile, Quick Look<https://www.microsoft.com/en-us/research/publication/a-quick-look-at-impredicativity/> depends strongly on simple subsumption. And I'm very keen on QL. Simon From: ghc-devs On Behalf Of Chris Smith Sent: 16 June 2021 14:39 To: GHC developers Subject: Is simplified subsumption really necessary? This might be in the "ship has sailed" territory, but I'd like to bring it up anyway. https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0287-simplify-subsumption.rst<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fblob%2Fmaster%2Fproposals%2F0287-simplify-subsumption.rst=04%7C01%7Csimonpj%40microsoft.com%7C6e04d0f9a068432fad8108d930cc2e1e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637594475810326243%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000=r6RfLGB0CRXF%2FN%2FFvbu3uDoxg1i63oVXya2v6Zlqr7E%3D=0> says: Suppose GHC lacked all four features, and someone proposed adding them. That proposal would never leave the launchpad. Let's test that hypothesis. I've been spending increasing amounts of time fighting against simplified subsumption while porting Haskell code to GHC 9.0. It's not that any specific instance of this problem is hard to fix; rather, it's that it completely screws up my intuition about what should be valid Haskell. It doesn't help that HLS still requires 8.10.4, so I usually don't find out I've broken my libraries for GHC 9.0 until continuous integration kicks in. At this point, it's become fairly routine that my code that works fine with 8.10.4 is broken with 9.0, and this makes me sad. Understandably, eta expansion reducing the strictness of terms is bad. But wouldn't it be possible to choose a desugaring with seq that doesn't do so? ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Is simplified subsumption really necessary?
This might be in the "ship has sailed" territory, but I'd like to bring it up anyway. https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0287-simplify-subsumption.rst says: Suppose GHC lacked all four features, and someone proposed adding them. > That proposal would never leave the launchpad. > Let's test that hypothesis. I've been spending increasing amounts of time fighting against simplified subsumption while porting Haskell code to GHC 9.0. It's not that any specific instance of this problem is hard to fix; rather, it's that it completely screws up my intuition about what should be valid Haskell. It doesn't help that HLS still requires 8.10.4, so I usually don't find out I've broken my libraries for GHC 9.0 until continuous integration kicks in. At this point, it's become fairly routine that my code that works fine with 8.10.4 is broken with 9.0, and this makes me sad. Understandably, eta expansion reducing the strictness of terms is bad. But wouldn't it be possible to choose a desugaring with seq that doesn't do so? ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
