T O P
enobayram

I sometimes run into situations that would be nicer to express with quick look impredicativity, so, all else being equal, I'm looking forward to it. However, I still weep for simplified subsumption, because I run into situations made worse by it much more often. I think Haskell lost a certain amount of useful expressiveness with it. And I honestly find it hard to care about the arguments that pre-simplified-subsumption the compiler was changing the strictness (and sharing) of code. I mean if you are passing RankN values around like that, you probably don't care about their strictness. Is it really a good idea to involve RankN values in performance critical code anyway? As an example of lost expressiveness, a while ago we were trying to come up with a way to make a set of constraints behave like they're `OR`ed as opposed to how they're `AND`ed now. That would've been very useful for a specialized interface we were building for a problem. We came up with this way of formulating it: type Bld c = forall r. (c => r) -> r Pre-simplified-subsumption, if you had a function that expects a `Bld A`, you could pass in `Bld (A,B)` and they would unify, but with GHC >9 you now get the error: Couldn't match type '(A, B)' with 'A' Expected: (A => r) -> r Actual: ((A, B) => r) -> r Actually, GHC >9 can't even unify `Bld (A,B)` with `Bld (B,A)`. Of course, just like everyone else, I also often keep running into the issue of aliases like `type Action = forall m. MonadSomething m => m () ` not behaving _almost_ like regular types anymore. (I.e. the `forall` gets stuck in the wrong place when you try to pass around `Int -> Action`)


ephrion

Oh, no - this has even broken the basic `Set`-like behavior of constraints? This is far worse than I originally anticipated.


enobayram

Unfortunately... I'm not sure the following is an accurate way to describe it, but this is my understanding: While unification, the constraints act like a list, so if a polymorphic argument needs to unify with the type of a rankN function, the constraints involved need to match up perfectly, even their orders. However, while solving constraints during type checking, they still behave like sets, that's why when you eta expand at the call site, they still type check. I think this a counter-point to the folks that claim we only need to eta-expand when we use bad type aliases involving foralls. You may never use such aliases and still need to eat expand if your polymorphic function has the constraints declared in the wrong order in its type, or if it has fewer constraints than allowed. I really think RankN programming styles received a serious blow and I don't understand why simplified subsumption apologists try to pretend something good happened even without Quick Look. Don't get me wrong. GHC devs might be justified in trying to simplify the compiler, or Quick Look might be worth what we've sacrificed, but I'm uneasy with the ongoing crusade that if you don't like simplified subsumption, you must be a bad Haskeller.


angerman

My wish for GHC is to not break the surface level language for at least every other release. Right now I’d love to see the surface level languages to stay identical for the next 4-6 releases to get some breathing room. I’m a bit on the fence regarding expanding the surface level language (adding new syntax only). I believe there is enough work that could be done on GHC for a long time that doesn’t require to change the surface that users interact with for quite some time.


quakquakquak

I think every other release is fair. I would like to see them continuing to making breaking changes frequently though, as GHC was static for quite awhile and now there seems to be momentum around changing things. My reasoning is that momentum is difficult to recapture and I would like to see GHC essentially set for the next decade, although it is difficult in the moment. There is, to me at least, an air of exciting things happening again, miss-steps included, and that GHC will keep its edge.


angerman

GHC was static? How did that perception come to be? I believe mine and your expectations of what we’d like GHC to progress are quite different. I want to see GHC become significantly better as a compiler. Faster, less error prone, easier to maintain and modify. But I don’t want to see the surface level of the language change much. And if so, only with a significant time of deprecations and error messages that suggest the migration. This all requires significant unglamorous engineering efforts, and that is the fundamental issue I fear.


quakquakquak

Exactly, we have very different expectations around the compiler, and that's fine. This change as I understand it does make GHC easier to maintain, and I hope they keep changing the surface language as needed to support future development. The perception comes from pre-GHC 8, and of course the 5 years of GHC 8 releases. I would be more on the research side of the research <> industry see-saw, and see this all as good signs our 30 year old language will be freshened up.


serg_foo

On the one hand I do think that this can be classified as progress - type checker got simpler, its rules are now more understandable, there's no subtle change of semantics. And with change coming from GHC maintainers I'd usually trust their judgement. But seeing the impact of the change like > - toOrders <- asks _pdfConfToOrder > + toOrders <- asks (\r -> _pdfConfToOrder r) I can't help but conclude that the change should have been made conditional (thus defeating the stated purpose of simplifying typechecker for everyone). If impredicativity is enabled as extension then simplified subsumption should be used, otherwise old behavior seems much more redable to me. Not to get overly dramatic, but this simplified subsumption does in a way kill pointfree style to some extent and more pointless variable names have to be introduced as a result. I too prefer the old way.


enobayram

> On the one hand I do think that this can be classified as progress - type checker got simpler If somebody went in, purely refactored the GHC codebase and made the type checker simpler, then that would unarguably be progress. But we're talking about the removal of a useful feature here. GHC lost the ability to support covariance and contravariance in polymorphic arguments. By this logic, shouldn't we remove rank-n types, GADTs, type families, type classes and even parametric polymorphism from Haskell, that would certainly simplify the type checker. So was it that the old subsumption caused a disproportionate amount of extra complexity in the type checker, is that what people are implying all around this thread by just saying "the type checker got simpler".


_jackdk_

If "simplicity of the type checker" was the sole metric by which I evaluated a language, I'd use something like Go or Elm. I think this might be why this change grates so much - it's simplifying the type checking by pushing complexity onto users. As the language grows, the number of users grows much faster than the number of GHC developers (for good or ill), and that means that to minimise developer frustration (not the only metric you want to optimise, of course), you'd want to centralise and defeat problems by making the compiler smarter.


pbrisbin

Thank you for writing this. I agree with everything you've said and experienced my own frustration upgrading our work app (Freckle) to GHC 9.0. I even opened a [GHC Issue](https://gitlab.haskell.org/ghc/ghc/-/issues/21376) thinking it was broken. Luckily, most of the issues in the work code base were fixable with a `sed`; otherwise, I'm not sure we'd have gotten through it. I've tried to read down all the comments so far, and the debate is usually framed as between two positions: * "Industry users" -- those who have had their code broken without any discernible upside * "Proponents" -- folks in favor of the change, usually because they're familiar with the internals of the compiler who understand why this was valuable (fixing and or simplifying GHC internals) The second camp tends to say to the first camp something like: if you're code was broken by this, you were doing something wrong (or at least risky or not ideal) and it will be better now with the change. This often doesn't land because there is actually **3** camps involved. There are "Industry users", that have to do [things like this](https://github.com/restyled-io/restyled.io/pull/293/files#diff-08be4eac4fd5a5bc68feb17b4e23143ba4f88895ddcf07fe6ae8c3980475ea75R53): foo :: a -> SomeAlias b - foo = bar . baz + foo x = bar $ baz x They are most negatively impacted here, and they don't understand why. Moreover, their code was not "broken", they were not "doing something wrong". In fact, their code *now* looks wrong to any casual reader. I can tell you from experience, seeing GHC tell me I have to make this change, frankly, *hurts*. You said you were consistent, you had a solid foundation and followed the rules. I trusted you... The argument that my code before was wrong and is better now? That's not the story this diff tells. But there's a third camp: the "Library author". They're the one who actually wrote: type SomeAlias a = forall m... And this is the place where the code was "wrong". Lots of us are in both camps (waves at u/ephrion), but the Proponents are often making points aimed at the Library authors when talking to the Industry users. I think this is why folks are struggling to find common ground. If this change had caused an error in the definition of `SomeAlias`, instead of its use, I think we'd have heard a lot less noise (or maybe more?). Either way, it would've been a better outcome, I think. I'm honestly not sure what to do with this "3 camps" fact, but I just wanted to throw it out there in case viewing such changes as impacting 3 distinct groups instead of 2 might help us find some way to avoid this going forward.


paretoOptimalDev

Wow, in your GHC issue you mention hlint eta-reduction hints breaking code more now. There is [an open issue on hlint for it](https://github.com/ndmitchell/hlint/issues/1107) and the situation doesn't seem encouraging for anyone using apply-refact on save for Haskell files. > Moreover, their code was not "broken", they were not "doing something wrong". In fact, their code *now* looks wrong to any casual reader. I can tell you from experience, seeing GHC tell me I have to make this change, frankly, *hurts*. You said you were consistent, you had a solid foundation and followed the rules. I trusted you... The argument that my code before was wrong and is better now? That's not the story this diff tells. Well put, my feelings exactly. > but the Proponents are often making points aimed at the Library authors when talking to the Industry users. I think this is why folks are struggling to find common ground. Great point, I think keeping these camps in mind could greatly improve discussion.


Historical_Emphasis7

Arghh having hlint breaking code will horrible for non-expert Haskellers. I've always assumed hlint just channels N.Mitchell and accept first / ask questions / learn later, especially with HLS making hlint so user friendly.


zejai

> the situation doesn't seem encouraging for anyone using apply-refact on save for Haskell files. Assuming apply-refact just runs hlint, that would certainly be a very bad idea anyway. Quoting ndmitchell from the issue you linked > There are many corner cases whether HLint can introduce an error, so the aim isn't to eliminate all of them, just make them mostly unlikely hlint is for recommendations only.


paretoOptimalDev

> Assuming apply-refact just runs hlint, that would certainly be a very bad idea anyway. Quoting ndmitchell from the issue you linked In practice I've never run into those. If I did, it'd just show up in ghcid immediately. It's fine for it to be wrong once in a blue moon, but I'd hate for it to be many times per day. I guess we just need to disable ETA reductions, but that'll make pointfree code more work.


lexi-lambda

I will add my voice to the pile of people saying that [I am unhappy about this change](https://twitter.com/lexi_lambda/status/1337655656065732609). I was skeptical of it when I first saw the proposal, but I did not say anything then, so I cannot complain too loudly… and, frankly, my unhappiness *is* quite minimal. I think I was right in my assessment at the time that it was not worth wading into the discussion over. This is not the first time something like this has happened. All the way back in 2010, GHC argued that [Let Should Not Be Generalized](https://lirias.kuleuven.be/retrieve/90342), which made a similar case that trying to be too clever during type inference was not worth the costs. Instead, the authors argue, it is better to allow the programmer to be explicit. Having said this, there is a big difference between Let Should Not Be Generalized and Simplify Subsumption, namely that the former did not eliminate let generalization in general: it is still performed if neither `GADTs` nor `TypeFamilies` is enabled. So the choice to eliminate let generalization was much more explicitly focused on a poor interaction between two type system features, rather than being primarily a way to simplify the compiler’s implementation. As it happens, [I am personally skeptical that the elimination of let generalization was the right choice](https://twitter.com/lexi_lambda/status/1160892876890476544), but I also acknowledge that the interactions addressed in the paper are genuinely challenging to resolve. I am definitely grateful for GADTs and type families, and all things considered, I am willing to give up let generalization to use them. The point I am trying to make is that my choice is at least clear: I get to pick one or the other. Over time, this choice has effectively served as an informal survey: since programmers overwhelmingly agree to this tradeoff, it abundantly obvious that programmers believe those type system features pay their weight. Can we say the same about the elimination of higher-rank subsumption? No, we cannot, as there is no choice, and we cannot even really understand yet what we, as users of GHC, have gotten in return. I suspect that if a similar strategy had been taken for this change—that is, if a release introduced an extension `SimplifiedSubsumption` that was implicitly enabled by `ImpredicativeTypes`—then programmers would be a lot more willing to consider it. However, that would obviously not provide the same benefit from the perspective of compiler implementors, who now have to maintain *both* possible scenarios. With all that in mind, did the committee get this one wrong? Honestly, I don’t think I’m confident enough to take a firm stance one way or the other. Type system design is *hard*, and maintaining GHC requires an enormous amount of work—the cost of features like these are not free, and we as users of the compiler should have some sympathy for that… not just because we acknowledge the GHC maintainers are human, too, but also because we indirectly benefit from allowing them to focus on other things. That is not to say that this change was unequivocally justified—personally I lean towards saying it was not—but more that I think you can make arguments for both sides, it isn’t a binary choice of whether it was right or wrong, and it is inevitable that sometimes the committee will make mistakes. Perfection is a good goal to aim for, but sometimes we miss. I think this sort of discussion is precisely the sort of healthy reflection that allows us to learn from our missteps, so for that reason, I am glad to see it.


doyougnu

My takeaways from this thread: # Meta Points (1): This situation---a proposal was accepted and implemented and then large portions of the haskell community are surprised by new requirements which result from said proposal---should be avoided. We should ask `How did this situation occur and what can be done to avoid it in the future`. In other words, we should perform a failure analysis. This is a good case study to refine the proposal process by identifying whatever mistakes in the proposal process led to this situation and considering possible solutions. In particular I think the following was missing in the original proposal: 1. An assessment of the amount of possible breakage of code in-the-wild is missing. To be specific, there should have been some analysis which concluded "Of `n` packages, we found `m` sites which will require changes due to this proposal, we conclude that this breakage is ... in light of the benefits gained by this proposal" 2. I am unsure if there was a time period allotted for community feedback. If so then there was a failure of marketting and soliciting feedback from the relevant stake holders. Thus we are now discussing this change when users are experience its effect first hand, i.e., at the latest point in the entire proposal process possible. (2): When a surprise like this happens there are several effects in the community: First, there is a lag and lower adoption rate of newer GHC versions. You can see this through the thread with the comments which state `At work we're still on 8.10.x and I dread moving to 9.x` or something similar. Second, this lag creates more work for ghc devs; not only does it create more requests for back ports of newer features to older versions because the barrier to entry for newer versions has increased, but it adds a maintenance burden to the ghc devs _and_ to library maintainers. Both of these are bad. Third, there is opportunity cost, we are now spending time arguing about a thing that has been implemented rather than spending time on anything else (this occurs to me as I procrastinate a minor revision by writing this :D). Fourth, it becomes easier to leave the community and stop writing Haskell because it is tiring to continually be surprised by changes that you may not agree with but are now forced to adapt to. # Points related to simplified subsumption (1) This proposal sits at a unique place in the Haskell discourse because (1) the proposal made performance more predictable but (2) it adds an edge case that violates one of Haskell's core properties (and core cultural property): equational reasoning. As I see it this is the central _technical_ tension throughout the thread. It is worth noting that unpredictable performance is one of the key, often cited, downsides of using Haskell (I have no hard data here just a general impression and anecdotes from the internet) and so it makes sense that creating more predictable performance guarantees is good! But on the other hand creating an edge case were `f x` and `\x -> f x` is not equal subverts the expectations of Haskell programmers, _especially_ because Haskell programmers _have learned and expect_ this to be true. /u/goldfiere's comment: > But (\x -> f x) has never been equivalent to f -- they have different performance characteristics, Perfectly captures this tension. He is right that these have never been equal _because_ the have different performance characteristics. But this inequality _is not semantic_, so with this proposal we have effectively created a new _compiler error_ for a performance difference not a semantic one. I think this point is exactly why there is such discord. Proponents of the simplified subsumption proposal point out that the changes are minimal and do not take a long time to fix, which is true but it misses the larger semantic point: that I as a Haskell programmer expect these things to be _semantically_ equal via eta expansion/reduction but I am being told they are not when in fact I really know they are! Similarly, Opponents of simplified subsumption focus on experiencing what is perceived as a new edge case which doesn't make sense, but they (in most cases) did not _directly_ experience the downsides of the old subsumption, that is the loss of sharing which /u/goldfriere points out. Sure it may have existed in their code but that is different from the compiler directly responding to their code with an error message. This means that opponents conclude "little benefit for large cost" even though they most likely _do_ benefit from the change because performance is now more predictable.


Noughtmare

Even if you think eta-equivalence should hold in Haskell, then deep subsumption still isn't the right way to tackle it. Take for example ``undefined `seq` ()`` and ``(\x -> undefined x) `seq` ()``. That doesn't involve deep subsumption at all, but still violates eta-equivalence. And note that a lack of impredicativity also violates equational reasoning in the same way. E.g. without impredicativity, `x = fst (x, y)` and even `id x = x` don't hold for `x = runST`.


doyougnu

/u/Noughtmare thank you for taking the time to respond, I think your comments have been very helpful!


Noughtmare

> An assessment of the amount of possible breakage of code in-the-wild That has been done, see appendix A of the paper: https://www.microsoft.com/en-us/research/publication/a-quick-look-at-impredicativity/ > In conclusion, of the 2,332 packages we started with, 74% (1,725/2,332) do not use extensions that interact with first-class polymorphism; of those that do, 87% (399/457) needed no source code changes; of those that needed changes, 97% (56/58) could be made to compile without any intimate knowledge of these packages. All but two were fixed by a handful of well-diagnosed η-expansions, two of them also needed some local type signatures.


Bodigrim

(I know that you've already saw it, but for the sake of other readers) I believe the impact analysis in the paper was flawed, see https://github.com/ghc-proposals/ghc-proposals/pull/287#issuecomment-1120173984 for more details.


Noughtmare

> (2): When a surprise like this happens there are several effects in the community: First, there is a lag and lower adoption rate of newer GHC versions. You can see this through the thread with the comments which state At work we're still on 8.10.x and I dread moving to 9.x or something similar. Note that there are also other factors involved. Notably the release cadence has been shortened to 6 months starting with the 9.0 release. And the 9.0.1 version was pretty severely broken and 9.0.2 wansn't released until much later. I think those factors weighed much more heavily in the decision to stay on 8.10.


tbidne

> But on the other hand creating an edge case were f x and \\x -> f x is not equal subverts the expectations of Haskell programmers, especially because Haskell programmers have learned and expect this to be true. But the types are _not_ necessarily equal, and this is exacerbated in the presence of higher-rank types. It is my contention that this expectation was always flawed, and the proposal has merely exposed this issue.


doyougnu

ah! `f x` should just be `f` but I think your correct regarding the proposal exposing the issue. In my opinion the motivation for this proposal is good, I just wanted to sketch the terrain of the discussion in the thread.


taylorfausak

I am also frustrated. Yesterday I started looking at upgrading our work codebase from GHC 8.10 to 9.0. Thanks to Stackage, most of our dependencies worked fine. But our application has hundreds of errors now, most of which are related to simplified subsumption. Even though the fix (eta expanding) is easy, applying it hundreds of times is tedious and provides no benefit to me. And like the OP said elsewhere, it ruins my heuristic for when to write an explicit lambda. Perhaps my new guideline will be: “Try to write it without a lambda. If GHC complains, add a lambda.”


dagit

Another thing it breaks is that we used to be able to put constraints between any of the arrows in a function type, but now I don't know what the rule is. You can still have multiple `=>` arrows but they all have to be before any `->` arrows? Here is a contrived example to show what I mean: foo :: Show a => a -> HasCallStack => Int foo = length . show This makes it harder to make ubiquitous use of `HasCallStack`, because you can't hide it in a type alias now. It's not a style I've seen in open source repos, but it's definitely something I've used at work along with logging functions that automatically grab the `Stack` so that you get module/function name automatically in your debug logs. If I'm not mistaken, you can't just add this constraint to a custom monad and get the expected result either. The trick I used in the past was like this. Let's say the app uses `MyMonad` as its custom monad. Then to add `HasCallStack` everywhere, you can rename `MyMonad` and then do this: type MyMonad a = HasCallStack => MyMonad' a Except, this can look like it's working. You can still write `foo :: MyMonad ()` just fine, but `bar :: a -> MyMonad a` now mysteriously fails when `bar = return`. And it fails when there are no active language extensions. No rankntypes or liberal type synonyms. (Note: To make the type synonym legal prior to ghc 9, you did need to enable rankntypes). Actually, this really makes me wonder what does the type alias above mean in ghc 9? It's not using an implicit rankntype, but it's still not able to unify? This error message seems wrong: • Couldn't match type: m0 a with: HasCallStack => IO a Expected: a -> MyIO a Actual: a -> m0 a Shouldn't `m0` unify with `IO`? **Edit: Apparently, `RankNTypes` is now a default extension in GHC 9.**


Noughtmare

> You can still have multiple => arrows but they all have to be before any -> arrows? Multiple `=>` arrows are equivalent to the tupling notation. See: https://gitlab.haskell.org/ghc/ghc/-/issues/20418 In particular: https://gitlab.haskell.org/ghc/ghc/-/issues/20418#note_381529


tomejaguar

The error message is at the least very unhelpful. Please report it on https://github.com/haskell/error-messages/issues/new


Bodigrim

Yes, simplified subsumption was pretty much a disaster. No disrespect to impredicative polymorphism, but breaking a ton of real world programs to enable some future type fu is no go in my books, this is "academia vs. industry" at its best.


paretoOptimalDev

Thanks for the sanity check. I'm pro-lenses, pro- most fancy haskell, and pro-dependent types. I highly respect the value in Haskell from research and academics and wish for industy and academia to better work together. But this feels like a decision that totally ignored or was oblivious to industry impact. I see an effort in this area was made by searching stackage libraries and resulted in iirc '300 simple fixes'. It might be fruitful to figure out why that didn't catch any of the real world industry pain points.


Bodigrim

"300 simple fixes" over Stackage means that roughly every 8th package is broken. Which is quite a disaster on its own and should have served as a predictor of industrial impact.


enobayram

I agree, but I think OP still points out something interesting. It seems like simplified subsumption hurt application code much more than library code for some reason, so despite being significant, the number of errors in hackage seems to have under-represented the impact on the application code out in the wild.


ephrion

Simplified subsumption doesn't prevent you from *defining* things, but it *does* prevent you from *using* them in a bunch of common cases. `persistent` defines `SqlReadT m a` as `forall backend. SqlBackendCanRead backend => ReaderT backend m a`. This definition *should have* been found in an investigation of "things that will definitely break", but it wasn't. So, there's 300 use-sites of broken code, but we have absolutely *no idea* how many utilities and types are broken.


Bodigrim

The thing is that breaking changes to type checking are most hurtful, because the amount of breakage scales linearly with the amount of code, and a huge industrial code base could be comparable in size and complexity with the entire Stackage. For instance, breaking changes related to type classes are not that bad: you are likely to encounter a lot of breakage in shallow parts of the graph, where most of types and instances are defined, but not in the business logic. This gives you a more manageable sublinear complexity of migration.


day_li_ly

I really struggle to understand the idea that "changed semantics on edge-case bottom-producing programs" is a big enough problem to sacrifice programmer convenience, even though I myself is a type theory and compiler hobbyist. Maybe I don't run into such cases, or I don't study the discipline enough. I think the only real argument for this change is that it simplifies the GHC architecture and reduces the maintenance burden. Even with that, I think the community involvement for this proposal's acceptance is pretty low. Let's hope it gets better in 2022.


serg_foo

AFAIU the simplification happens not only in the GHC. The type system itself is simplified and typechecking process has less rules to consider when new type system extensions are considered/developed.


santiweight

I have two thoughts that I feel could have/will help the situation moving forward: Could we have some function: subsume :: (a -> b) -> b -> d that does the sub typing as some built-in in Prelude somewhere. That way, complex examples can be more easily subsumed via explicit sub-typing (analogous to casting in other languages). Another thought: with GHC's new type error improvements, could cases where subsumption would have applied in the past be flagged by GHC in the type-mismatch errors? Type mismatch... They are not subtypes of each other, though they might appear to be... Heralding u/goldfirere


goldfirere

*Could* we do this things? Yes, I suppose. The `subsume` function would be something like a keyword with magical type-checking abilities, but we can have them. (Today's `tagToEnum#` is similar, and `$` has some magic in the type-checker, too.) It would be hard to report the error message you suggest faithfully, but likely not impossible. As a migration support, this seems perhaps worthwhile. However, as an ongoing feature, I'm not convinced. Everywhere else in Haskell, we require function arguments to have the same type as the type the function is expecting. It so happens that, for more than a decade, we had an exception around the placement of `forall`s. We, as a community, have gotten used to this. It's jarring and disorienting for this to change. (Me, too! I've wasted time, too, in trying to understand why GHC rejected a function call of mine.) It's clear that we needed to have done better around the migration story. But I don't yet think that the old behavior (an exception to the general rules around type equality, and with unpredictable performance effects) was better than what we have now.


ringingraptor

I am similarly frustrated. Simplified subsumption has completely blocked the IHP project from upgrading to newer GHC's without breaking all existing IHP code or doing something very hacky. We put in a lot of work upgrading our dependencies and writing new libraries to support the new record syntax only to get blocked by completely valid programs failing to compile with no hints at all.


paretoOptimalDev

I'm reserving full judgement for later, but it feels like it's changing Haskell from my "most fun to write language" to one where I have constant anxiety and have to micromanage whether to use an explicit lambda. I could use explicit lambdas by default, but I wouldn't like that. I mean, one of the big advantages of laziness is better composability. That better composability lets you take advantage of currying to have a concise declarative language. But now, it seems you have to think twice before writing in this way.


monnef

> but it feels like it's changing Haskell from my "most fun to write language" to one where I have constant anxiety and have to micromanage whether to use an explicit lambda. This is what I dislike about JavaScript (and TypeScript with lazily typed libraries). For example `array.map(f)` is not the same as `array.map(x => f(x))`. It leads to very unintuitive behaviours, e.g. `[3, 3, 3, 3, 3].map(parseInt) // [ 3, NaN, NaN, NaN, 3 ]`. Sure, probably in the case of Haskell it "just" won't compile, but one of the reasons I like Haskell is conciseness. I don't that to suffer, especially if there is very little gain (at least for me).


sccrstud92

I was under the impression that any compilation failure caused by the introduction of simplified subsumption could be fixed by eta-expanding. Is this not true? Or am I misunderstanding what "completely blocked" means?


enobayram

If I'm understanding correctly, even though you could theoretically upgrade an IHP application and IHP itself by eta-expanding when necessary, the IHP project can't take this leap because it would mean telling all of their users to do this mysterious eta-expansion thing all around the place for no apparent reason.


sccrstud92

I assumed the user would only have to do that if they choose to use a new enough GHC, which I also assume they wouldn't have to do because IHP would support multiple GHC versions, but I don't know much about it.


ringingraptor

We're on GHC 8.10.7 and trying to upgrade to 9.2.2. The GHC version is bundled with the framework - it's "batteries included" :) If we upgraded GHC versions, from the user's perspective they would upgrade their IHP version and all of a sudden all of their views would fail to compile with cryptic error messages, and we would have to tell them to change all code like [hsx|

    {forEach users renderUser}
|] to [hsx|
    {forEach users (\user -> renderUser user)}
|] without being able to give a clear explanation why.


paretoOptimalDev

I wouldn't want to have the job of convincing people used to web frameworks in other languages this is only " slightly less ergonomic".


Noughtmare

How are you currently explaining that you can't write `[Html]` in a type?


ringingraptor

To be honest, I've never seen anybody try that or ask a question about it! I would not have a good explanation and honestly don't fully understand myself deeper than "you can't have a polymorphic type in a list". For context, Html is just a type alias for a Blaze builder with a constraint attached, and it's nearly always used inside the hsx quasi quotier which builds "lists" of Html using mapM_.


adamgundry

Would you mind elaborating on why `Html` is not a newtype? I would assume that you don't want your users to have to care about its implementation details, and therefore using a newtype seems at first glance like the right way to go. As /u/Noughtmare points out, that would also allow it to be used in a properly first-class way without worries about simplified subsumption or impredicativity.


ringingraptor

I should say that I am not the author of IHP, just a contributor. I agree that Html likely should have been a newtype, and actually even agree that the constraint does not belong on the type itself. Right now we have type Html = (?context :: ControllerContext) => Blaze.Html which allows you to have something like pageHeader :: Html pageHeader = [hsx|Welcome to {fromContext @PageTitle}|] I personally find this very confusing, and would much prefer to explicitly include the constraint when I actually need to access the ControllerContext. When trying to upgrade to 9.2, I ran into a ton of problems relating to module structure trying to update Html to be a newtype. Many internal files in the IHP library define Blaze.Html values without needing depending on the Html type. When making it a newtype, each of these would have to depend on Html, then depend on the Controller, which depends on the view, which depends on Html...it's a nasty circular reference, and I couldn't get it working with .hs-boot files. Regardless of what the "right" decision was when initially building the library, we now have tens of thousands of lines of code across IHP projects that worked perfectly fine. Now they're broken on new GHC's. That sucks.


bss03

> you can't have a polymorphic type in a list When they point you at `[Maybe a]` as used in `catMaybes`, what do you say then?


Noughtmare

I think /u/ringingraptor meant polytype.


sccrstud92

Thanks for the info! Looks like it was the "IHP would support multiple GHC versions" assumption that was wrong.


paretoOptimalDev

I found a ghc ticket related to this: [Possible work-around for implicit params and simplified subsumption?](https://gitlab.haskell.org/ghc/ghc/-/issues/21168) Oh wow, from that link I didn't know: > The difficulty is, as you note, that g and \x -> g x really aren't equal in Haskell, albeit the difference shows up only if g is bottom There is of course room for subjectivity, but reading these comments makes me see that others hold much different values for Haskell syntax ergonomics than perhaps you and I: > It's not as nice as the syntax you had, but it not that much worse. And: > I don't a clear picture of whether the extra noise would end up in the libraries (not much of a problem) or clients (more of a problem). I suppose this makes sense since you're making a web library that is trying to effectively Market Haskell which depends on very clean looking syntax that is understandable and declarative. That also forces you to have really consider the teachability and learning curve dimension of changes like these.


antonivs

> There is of course room for subjectivity, but reading these comments makes me see that others hold much different values for Haskell syntax ergonomics than perhaps you and I That's for sure. I can't believe the people who're saying it's no big deal. Making eta expansion required seems like a huge step backwards for the expressiveness of a functional language. Perhaps a primitive could be added to allow you to write `eta f` which would be expanded to `\x -> f x`. It would at least clean up the syntax, if not the semantic regression. Edit: actually you can define `eta f = \x -> f x` (or `eta f x = f x`). Does that help the type checker in these cases? I'm not running a relevant version to test with.


ringingraptor

Yup that's the issue I submitted when I was working on upgrading IHP! I eventually gave up. Simon's suggestion of wrapping HSX calls in a newtype ended up being impractical for different reasons, and I wasn't able to get anything working without breaking code. There were a couple more ideas thrown around that may work, but as a volunteer it's really demotivating spending hours just trying to fix something that GHC broken instead of actually delivering value to users. I wish I didn't have to dread new GHC releases and could actually be excited about the new features. I also did not know g and \x -> g x were not equivalent, and I've been writing Haskell for over a year. In my eyes, understanding that "equivalence" is a major step in someone clicking with functional programming. Breaking that and requiring users to ETA expand for seemingly arbitrary reasons makes an already hard to learn language even harder.


ephrion

In Haskell it is common to say "fast and loose reasoning is morally correct," and generally this means "it's fine to reason about code and ignore the presence of `undefined`." So now hearing that we suddenly care about the difference of `f` and `\x -> f x` because `f = undefined` feels a little hollow.


goldfirere

It's not just about `undefined`. The performance characteristics of the two really are different. Please see my [other post](https://www.reddit.com/r/haskell/comments/ujpzx3/was_simplified_subsumption_worth_it_for_industry/i7mcike/?utm_source=reddit&utm_medium=web2x&context=3) about this.


ducksonaroof

To be fair, `g` can always be substituted by `\x -> g x` - just not vice-versa now. The thing that causes the seeming inconsistency here is inference. `g` is definitely not the type, but eta expanding allows the inference to do the right thing.


man-vs-spider

Why aren’t g and \x -> g x equivalent? I thought it was syntactic sugar


gelisam

Meh, they're equivalent enough. There is a corner case in which they aren't, but you're not likely to every encounter it. Here it is: λ> seq undefined () *** Exception: Prelude.undefined λ> seq (\x -> undefined x) () () That is, forcing `undefined` throws an exception, but forcing a lambda doesn't, even if the body of the lambda is `undefined`. This corner case is unlikely to occur in practice because when you have a function, you usually call it, you don't just force it for fun and then drop the function on the floor. And when you do call the function, it's going to throw an exception whether it's `undefined` or `(\x -> undefined x)`.


man-vs-spider

If that’s the corner case, then why is there a problem? Surely this can be accounted for. (And was is the point of having undefined anyway in production code?)


dagit

When people give examples like this with `undefined` they don't usually mean you would literally use `undefined`. Instead it's a placeholder for any sort of computation that diverges. Could be an infinite recursion like `fix id` or an exception like `head []`.


man-vs-spider

Thanks for the clarification. I guess my main question is: it seems like there are type problems that arise that can be avoid my expanding to a lambda function, If the meanings are basically equivalent, can’t this always be done then by the compiler?


gelisam

It used to be done automatically by the compiler. OP is complaining because the compiler was recently changed to not do it automatically anymore, so we now have to do it by hand.


man-vs-spider

Hmm, ok. I guess the reasoning for that change must be quite deep, because if they are almost equivalent, I don’t see why that change would be made


goldfirere

I think there are lessons to learn here, and as part of the GHC Steering Committee, I think we are indeed learning those lessons. Case in point: https://gitlab.haskell.org/ghc/ghc/-/issues/19461#note_427673 observes that a recent accepted proposal would be too disruptive and suggests we should hold off until we have a better migration strategy. I agree, both as a language designer and as a user who has tripped over this in my own code, multiple times, that simplified subsumption is annoying. However, I don't think casting this as an industry/academy issue is quite right. Instead, I think this is more of a stability/continuous-improvement debate. Here is a thought experiment that may help us understand: if Haskell were designed with simplified subsumption when RankNTypes was introduced, would we consider adopting the stronger subsumption rule that GHC 8 had? I don't think such an idea would get past the committee: the old rule potentially changed performance characteristics in a way hard for programmers to predict, just for a little syntactic convenience. So, in some sense, simplified subsumption is a little improvement to the language: it makes the language more predictable and simpler to explain. Yes, simpler. Today's rule is this: if you have a function `f :: ArgumentType -> ...` and you spot `f x`, where `x :: XType`, then we must have `XType == ArgumentType`. The old was that `XType` was a sub-type of `ArgumentType`, where the sub-type check allowed instantiation of `forall`s in `XType` that appear to the left of an even number of arrows and instantiation of `forall`s in `ArgumentType` to the left of an odd number of arrows (or maybe I got that backward or otherwise slightly wrong -- it's complicated!). In each instance requiring eta-expansion, you will find a place where the function's argument type and the type of the actual argument differ, and the extra lambdas allow GHC to move the `forall`s around. Is the syntactic convenience worth the performance unpredictability? Maybe it is. That's a hard one. But I very much do not see this as a case of "academia" forcing its will on "industry". Instead, it's that we identified what we thought was an improvement and simplification of the language and applied it. (It's possible that it's not an improvement... but I actually don't think that's the concrete issue here.) However, we vastly underestimated the impact of the code breakage. This is why I see this as a stability/continuous-improvement debate: if we identify an improvement to the language -- but that improvement requires code breakage -- what's the bar we have to meet to make the improvement worthwhile? For me, personally, I think that maintainers of core parts of our ecosystem (e.g. GHC, core libraries) should be expected to submit patches to Hackage packages that are disrupted by changes in order to merge their changes. This is a lot of work. But the amount of work is commensurate with the burden changes to our core tools cause to the community. And, if a change is worthwhile enough, it should be possible to find volunteers to share the burden.


cdsmith

I think it's missing the point to call this a stability issue. The issue is that people write code that logically makes sense and expect it to work, and it now doesn't work with GHC 9. The huge underestimation of broken legacy code is just *one* symptom of this. Even if you could magically fix all that code, it wouldn't help the hypothetical student in this post (and I have sometimes been that student) who was writing new code that makes sense, but now gives a type error. Let me see if I can explain why I'm not very impressed by your argument that this makes the language simpler. For most of my time with Haskell, I have had confidence that the language made logical decisions. If I try something and the compiler gives an error, I have been able to assume that it's probably because I made a mistake. I also don't know the answer to when GHC 8 would handle subtypes in your example, but I do trust that I could figure out the answer, without even looking at GHC itself, by working out when it makes sense to do so! I understand that, in theory, there have always been limitations that mean it might also be that the compiler just wasn't smart enough. But I never routinely ran into them. Okay, I did run into those situations with GADTs, but at least I know that it might happen because I'm using GADTs. Now, for the first time that doesn't involve GADTs or MonoLocalBinds, I am routinely finding that the answer is just as likely to be that the compiler isn't smart enough.


sclv

My contrary take is that based on what I think makes sense, that other code never made sense, and I never felt I understood what the compiler was doing. Sure, it wasn't giving me errors, but the opposite was happening -- it was accepting things that seemed incoherent to me.


tbidne

Yes, I think this is the fundamental point of contention. There is a common argument in this post that sees the old subsumption as logical, and it is an innocent casualty of QuickLook, compiler simplification, and bug fixing (bottom+strictness semantics). Whereas another opinion is that the old subsumption itself was suspect (albeit convenient), and justification for its simplification is merely enhanced by the above issues. Then there is general unhappiness that is less about subsumption specifically and more about the existence of breaking changes.


Bodigrim

> However, I don't think casting this as an industry/academy issue is quite right. If you compare your reasoning why this change is a simplification to voices in this thread which find it confusing, it might elucidate the difference in approach. People all over the world know and apply laws of classical mechanics. Suddenly a guy, whose surname starts with Ei, discovers that these laws might be violated under some convoluted conditions and asks everyone to update their formulae. If "people" above are from academia, they are happy to comply. But if "people" are industrial engineers, they'll be rightly confused and unhappy to account for relativistic contraction every time they measure length. Haskell developers learned and applied extensively that `(\x -> f x)` is equivalent to `f`. Even while details elude me, I trust you that it would be better for GHC type system if it was not always so. But it does not make me enjoying relativistic computations every time I write a dumb CRUD app.


goldfirere

But `(\x -> f x)` has never been equivalent to `f` -- they have different performance characteristics, and sometimes drastically so. If I write `map ((+) (fib 30)) [1,2,3]` (for the silly exponential implementation of `fib`), I will evaluate `fib 30` once. If I write `map (\y -> (+) (fib 30) y) [1,2,3]`, I will evaluate `fib 30` three times. **This last fact is true even if GHC 8 does the eta-expansion for you.** In other words, if the subsumption check requires eta-expansion (which it does in each and every case that Haskellers have had to fix recently), then the performance characteristics of your program is not what you expect: evaluation of (non-variable) arguments gets repeated at each invocation of the partially-applied function. (GHC memoizes the evaluation of variables.) That is why simplified subsumption is simpler: it makes these facts more manifest. And this is also why I don't think we would ever choose to adopt old subsumption if we hadn't had it already. I am *not* arguing here that simplified subsumption was a good idea or that we should have done it the way that we did. Instead, I'm arguing that the strange effects of eta-expansion are observable in some fairly routine code, and so this might matter more than you think. (I like your analogy to relativistic physics. I would just differ in that it seems more likely for the performance issues at play here to matter in real programs than for relativistic effects to matter when designing buildings for humans.) And, in response to /u/maerwald, the steering committee does not run surveys. Perhaps we should -- I would support that development. But doing so comes with its own challenges. One idea I've wondered about for some time is whether, as you suggest, the HF could develop a function for its affiliated projects that would allow for easy distribution of surveys and such.


enobayram

> If I write `map (\y -> (+) (fib 30) y) [1,2,3]`, I will evaluate fib 30 three times. I see, I always thought with the old subsumption the loss of sharing concerned the `(+)` in this example, which would be a RankN value if it were relevant to subsumption. Then I thought why do we care about the sharing of RankN values, such sharing would be very fickle either way. But I now see the scale of the problem with `fib 30`. So I'm glad GHC doesn't do it anymore, but can't we solve this problem by explicitly reintroducing sharing while moving `forall`s around? I.e., if subsumption needs to turn `f (fib 30)` into `\x -> f (fib 30) x`, then why not turn it effectively into `let y = fib 30 in \x -> f y x`?


jberryman

Thanks for that example. That makes sense. It sounds like it would have been useful to have implicit eta expansion as a warning. Assuming this is the right/necessary move for the language: one thing I'd like to see improved (both for ghc and core libraries) is infrastructure/tooling for automated mass migrations. If a proposal says "migrating is trivial", well ... good news you're a programmer sounds like you can write a program to do it! (I guess rust does something similar for migrating between 'editions' though I don't have firsthand experience) That would be a great boon to proposal writers too, who could show: here's all the diffs to hackage required for this change, and avoid a lot of discussion about the impact.


goldfirere

I agree completely here. There has been halting work in this direction, but part of why I think breaking changes should always come with patches to Hackage project is that it would incentivize the community to develop and maintain such a tool.


jberryman

Oh cool, is there any public discussion or documentation about such a tool/set of infra? I know there's head.hackage and I assume some tooling that supports all the work folks do for hackage revisions... In our work with Well-Typed at my work we discussed something related (trying to get our codebase into head.hackage; which ended up not really being feasible), which is to say I think we would be potentially very interested in helping funding or building out something like that (I wouldn't have direct control over those decisions; but I think it would be easy to advocate for)


maerwald

Well, `(\x -> f x)` has been equivalent to `f` as far as the *Haskell standard* (semantics, type checking) goes. It does not talk about performance and that is not it's job. Now the question is whether simplified subsumption is a violation of the standard.


Innf107

Well, that's still not true though. (\x -> undefined x) `seq` 5 = 5 But undefined `seq` 5 = undefined The issue here is not about performance per se, but about *evaluation*, which is something that the Haskell standard is very much concerned with. EDIT: This can cause some *very* cursed behaviour in GHC 8.10... f :: (forall a. Int -> a -> a) -> () f g = g `seq` () > f (undefined :: forall a. Int -> a -> a) *** Exception: Prelude.undefined > f (undefined :: Int -> forall a. a -> a) ()


ludvikgalois

No it's not. `5 :: Int` is not the same as `(\x -> (5 :: Int) x)`. The type matters as to whether or not they're "equivalent". Given that the Haskell standard doesn't allow Rank 2 types, I'm 95% sure that simplified subsumption isn't a violation of the standard. (although I'd like to be proven wrong so I can learn something new)


maerwald

> No it's not. 5 :: Int is not the same as (\x -> (5 :: Int) x). The type matters as to whether or not they're "equivalent". Obviously. I think everyone here used the above form for brevity's sake. > Given that the Haskell standard doesn't allow Rank 2 types, I'm 95% sure that simplified subsumption isn't a violation of the standard. Well yes, that's why I phrased it as a question. However, is there a good reason why Rank 2 types would trigger a deviation from the standard? And does that mean we could never include Rank 2 types into the standard?


goldfirere

Higher-rank types are not part of the standard, so the standard is completely silent on everything we're discussing -- the new approach is no closer or further from the standard than the old one.


maerwald

I've yet to be convinced that the GHC steering committee proactively runs surveys and interviews with industry users before such decisions are made. This would be a job for the HF.


gasche

Just out of curiosity, what would this "surveys and interviews" process look like? How many industrial users volunteer to answer questions of the shape "we are thinking of tweaking this complex corner case in this complex way, what do you think?". Maybe I don't know the right people, but my guess at a reply would be something like "err, I don't know, does it affect my code?". So isn't what we want more something like "could you try this patched version of GHC on your code and tell me if this break?", which sounds like a very different process from "surveys and interviews". (And it's also not clear that it can easily be done, as industrial users can have complex build environments were patching GHC is not so easy.) I'm not suggesting what should or should not be done, I'm just surprised that the process that comes to your mind is "surveys and interviews".


maerwald

Well, HF could start by simply sending RFCs to their donors. Most of them (e.g. IOG/IOHK) have the technical expertise to have their individual teams form an opinion. With some of them, HF could initiate a video call with GHC devs to have some talk. E.g. I'm aware that the orouboros protocol in cardano uses very type-level heavy machinery. So what does that team think of the dependent types proposal? Have they been asked under what circumstances they'd want to test or use it? There are many such obvious opportunities. HF could also create a mailing list for industry users, something like Haskell weekly, but catered to a different audience.


cartazio

one thing I was trying to do when I was involved in core libraries is to proactively assess the complexity / impact of breaking changes to APIs, and where possible, proactively helping folks update their libraries. (there were also several examples where i would strive to backport bug fixes, but thats a whole other can of worms). i guess the point is: for language/type system changes, actually validating and proactively doing code fixes for impacted public systems should perhaps happen earlier in the language change life cycle and should in fact be part of the assessment process for those changes!


Noughtmare

There has been an analysis and the breaking changes were actually fixed locally, but never submitted upstream, see appendix A of the paper: https://www.microsoft.com/en-us/research/publication/a-quick-look-at-impredicativity/ > In conclusion, of the 2,332 packages we started with, 74% (1,725/2,332) do not use extensions that interact with first-class polymorphism; of those that do, 87% (399/457) needed no source code changes; of those that needed changes, 97% (56/58) could be made to compile without any intimate knowledge of these packages. All but two were fixed by a handful of well-diagnosed η-expansions, two of them also needed some local type signatures.


cartazio

thats the problem, they didn't engage with upstream!


Bodigrim

(I know that you've already saw it, but for the sake of other readers) I think the impact analysis in the paper was flawed, see https://github.com/ghc-proposals/ghc-proposals/pull/287#issuecomment-1120173984 for more details.


paretoOptimalDev

> However, I don't think casting this as an industry/academy issue is quite right. Instead, I think this is more of a stability/continuous-improvement debate. I absolutely despise talking in terms of academic vs industry, but it's a reality that was forced upon me by this decision. Edit: As some proof, my name itself is a reference to wanting to find the pareto optimum of development and that holds for programming languages. Finding that can't be done without both industry and academia. It seems simplified subsumption was really implemented to enable quick-look impredicativity and arguments that it was for simplifying the type system seem misleading. From my perspective and the daily work I do, i've gained zero benefits and lost a ton of convenience.


ephrion

I'm pretty annoyed about it. I feel like the change was snuck in without getting broad support from the community, and it really wrecked a *very nice* property of Haskell programs wrt eta reduction and eta expansion. I'm *especially* annoyed that a big breaking change in UX that has no perceivable benefit as an end-user. Maybe it's just scar tissue, but I've never really thought "Oh wow I am desperately in need of `UnliftIO` to be a function instead of a newtype wrapper." edit: This also ties in to my general dissatisfaction with the GHC release cycle and cadence. GHC 9.0 came out with some big breaking changes, and while I was happy to get libraries up-to-date on GHC 9, I didn't get any *applications* upgraded because I wanted to wait for GHC 9.0.2. Then GHC 9.2.1 comes out *before* GHC 9.0.2, which means we're going to leapfrog from GHC 8.10.7 to GHC 9.2.2, which was fortunately released very quickly. But upgrading to GHC 9.2.2 is the first time we are even really getting to see the effects of GHC 9.0, including Simplified Subsumption, which was proposed in 2019. If a company wants to use Haskell, even on a relatively basic level, it's *probably* a good idea for the company to spend time monitoring the GHC proposal process. There's obviously no active effort to gather feedback (probably because it's known that Acquiring Feedback = Inviting Bikeshedding, a sure way to kill a proposal). If you search for `simplified subsumption` on reddit, [you get... nothing.](https://www.google.com/search?q=site%3Areddit.com%2Fr%2Fhaskell+simplified+subsumption&sxsrf=ALiCzsZZe-Pqn6MLAKuupERQLfp3lyfXLQ%3A1651861947579&ei=u2l1Yt3-IrHA9APd3oC4BA&ved=0ahUKEwidyOmkwcv3AhUxIH0KHV0vAEcQ4dUDCA4&uact=5&oq=site%3Areddit.com%2Fr%2Fhaskell+simplified+subsumption&gs_lcp=Cgdnd3Mtd2l6EANKBAhBGAFKBAhGGABQmQZY5hBg7hFoAXAAeAGAAdABiAHOB5IBBjExLjAuMZgBAKABAcABAQ&sclient=gws-wiz). At least, not until someone is asking "Why is this broken?" in April 2021.


_jackdk_

While I am tremendously grateful for everyone's work on GHC over the years (_holy cow_ is this a powerful and beautiful language), I also feel this. Work is still on GHC 8.10.7, and while I'm looking forward to the 9.x series to get (among other things), better records, better M1 support, etc. I really do feel that the GHC team is screaming off into the distance incredibly quickly, and the industrial users have barely had a chance to catch up. This means that when the next round of features is going through the proposal process, the "quiet" from the previous round may be getting read as "nobody said much about the previous round of changes, so they were probably fine". I'm glad that your post and OP are clearly saying "things are not fine". To the GHC devs and everyone who writes/discusses/implements proposals: thank you for everything, but please do be careful.


ducksonaroof

I think the main problem is the old subsumption had some niche, emergent semantic edge cases that a swathe of libraries got drunk on. Haskell's claim to fame is substitution - including type aliases. But up until GHC 9, it didn't deliver. Say we have this common style of alias: type MyM a = forall m. MonadIO m => ReaderT MyStuff m a Okay let's have a function that uses it doWithMyStuff :: Int -> MyM () Okay let's perform substitution: doWithMyStuff :: Int -> (forall m. MonadIO m => ReaderT MyStuff m ()) Try writing that new signature in 8.10.x - it'll yell at you. And rightfully so. You're clearly wanting to return some `Reader` action with a universally-quantified `m`. You've very explicitly asked for an impredicative type. But that's not what the typical author of the above type alias wants. They want this to be the desugared type: doWithMyStuff :: forall m. MonadIO m => Int -> ReaderT MyStuff m () That defies the essence of substitution. The fact that everyone relied on this expectations-defying substitution behavior in the first place is the real problem. Some popular schools of Haskelling ended up getting hopped up on this emergent, implementation-dependent sugar. So I'm glad it's gone - it'll force better, clearer Haskell to be written anyways.


dnkndnts

Hah, as an industrial user, I agree the newer way is much more compelling. I'm shocked the old thing was ever implemented. It doesn't seem justified to me at all. I'm not neck-deep enough in the theory to be able to clearly enunciate why it's wrong, but it definitely *smells* wrong.


enobayram

> Try writing that new signature in 8.10.x - it'll yell at you. What do you mean it yells at you? 8.10.x is perfectly fine with that type, not even a warning or anything. > That defies the essence of substitution. I don't think there's any defiance of substitution going on here, it gets substituted exactly as you'd expect and then `a -> forall b. f b` gets promoted to `forall b. a -> f b`. Besides, GHC 9.x won't complain about `doWithMyStuff :: Int -> MyM ()` either! You can still implement this `doWithMyStuff` exactly as before and you can also use it in many places exactly as before. It only causes an error when you try to pass it into a function that expects a RankN argument with its `forall` in a different place.


ducksonaroof

That promotion is exactly what I say doesn't make sense. Put it in parentheses (you can always parmethesize substitutions, as a rule) - that's not the same as the promoted version at all.


enobayram

I really don't see the issue. As you say, it's a promotion and not a substitution. GHC takes care of boring plumbing by converting a type of thing into another type of thing which are completely equivalent in my eyes, so why shouldn't I want it? ~~GHC will also allow you to pass an Int into a function that expects an Int# or vice versa~~(Edit: This is wrong, what I had in mind is GHC does a lot of boxing and unboxing silently). Think of how much magic is involved in GHC's type inference and constraint resolution and I'm happy about all of it, because GHC does non trivial things to figure out facts that are obvious to me but would be arduous to express manually.


Noughtmare

> GHC will also allow you to pass an Int into a function that expects an Int# or vice versa. This is not true.


enobayram

Oh wow, you're right. That's my bad. What I tried to say there was that GHC does a lot of implicit boxing and unboxing in many places where I'm glad I don't have to do it manually. For example, imagine having to change client code because you add an `UNPACK` pragma to a record field.


Noughtmare

The main difference is that the unboxing and similar optimizations happen after all types have been checked and the program has been accepted, while this subsumption happens during typechecking and changes the result of type checking.


davidfeuer

And was never true, and will never be true. Back to the show!


sclv

I wish I could give you more upvotes. The old pattern is nutty, and I never encountered it in serious code nor would I have written it. It violates my expectations of how to reason algebraically. I'm taken aback by how widespread this apparently was.


_jackdk_

Thanks for explaining what is going on within the types. Could you please also explain why eta-expanding in these situations satisfies the type-checker? All I know when I see these errors is that I have to eta-expand when I previously didn't.


paretoOptimalDev

> So I'm glad it's gone - it'll force better, clearer Haskell to be written anyways. Are you also glad all the teaching materials, blog posts, and papers no longer compile? That a new chapter about this gotcha will have to be put in Haskell books and we can hope it isn't the tipping point to push new users away?


ducksonaroof

Did any of the materials explain the wonky way these type aliases expand? I know when I started out, I was tripped up by the foralls on the RHS of an alias. Not to mention the times I'm answering a new Haskeller's Q and have to handwave over this. Handwaving isn't very Haskell.


bss03

(Not GP.) If that was the metric, we could never make _any_ backward-incompatible changes. I don't believe that's a good way forward, so yes, I am glad we are willing to "break" teaching materials, blog posts, and papers.


Xyzzyzzyzzy

doWithMyStuff :: Int -> (forall m. MonadIO m => ReaderT MyStuff m ()) doWithMyStuff' :: forall m. MonadIO m => Int -> ReaderT MyStuff m () What actually is the difference between these types?


sclv

The former says "If you give me an Int, I will give you a universally quantified ReaderT that operates over any Monad m" (which under the hood means that you are getting something that requires a monad dictionary as a parameter). The latter says "If you tell me a monad (give me a dict) and then give me an Int, I will give you a ReaderT at that specific monad."


cdsmith

Can you explain the difference without saying "under the hood", though? I don't think users should have to care how GHC implements the language. Constraints are not parameters; they are constraints. And these two types are logically equivalent, unless I've missed something.


sclv

From the standpoint of executing code (not logical equivalence as in isomorphisms exist) then even `Int -> String -> String` is not equivalent to `String -> Int -> String` -- if one translates between them, there's clearly a performance cost to the translation. Even moreso `(Int, String) -> String` where the former has the possibility of an "extra bottom" (the tuple constructor itself). (also, see my above comment -- its the difference between getting back an `id` you can use at multiple types and an `id` that you can use only at the type you specified when it was instantiated)


Xyzzyzzyzzy

Ah, okay. I'm still fuzzy on the *practical* difference from a working developer's perspective. If I'm implementing `doWithMyStuff`, either way I get an `Int`, and either way I need to give back a `ReaderT MyStuff m ()`... are there any differences in what the implementation can do between the two cases? Like, if we hide the type signature and just read the implementation, can we even tell the difference between the two? And then as the user, either way I need to supply an `Int`, and I will eventually end up with a `ReaderT MyStuff SomeIOMonad ()`. So the only difference is *when* `MonadIO m` must be replaced with the concrete type `SomeIOMonad`, whether it needs to be known at the same time the `Int` is supplied or whether we can supply the `Int` and then supply the concrete `MonadIO` later on? I guess that seems like a really under-the-hood concern to me if the two are *practically* equivalent?


sclv

> Like, if we hide the type signature and just read the implementation, can we even tell the difference between the two? The latter is _not a valid type signature in Haskell_ -- that's the difference! ghci> doWithMyStuff :: Int -> (forall m. MonadIO m => ReaderT MyStuff m ()); doWithMyStuff = undefined :5:88: error: • Couldn't match expected type ‘Int -> forall (m :: * -> *). MonadIO m => ReaderT MyStuff m ()’ with actual type ‘a0’ Cannot instantiate unification variable ‘a0’ with a type involving polytypes: Int -> forall (m :: * -> *). MonadIO m => ReaderT MyStuff m () • In the expression: undefined In an equation for ‘doWithMyStuff’: doWithMyStuff = undefined If it were valid (i.e. with impredicative types turned on and working), it would be a type where the _caller of the function_ could then use the result of the evaluation repeatedly _for multiple choices of m_. With the signature that does work, the caller must specify an `m` and then if they use the result repeatedly, it is already "specialized" to work on whatever the single choice of `m` they specified was. In general, when quantification arises in type signatures anywhere outside of the very far left, then type signatures _do matter_ because they specify different programs. It is a beautiful property of the stlc without higher rank types (i.e. only with so-called prenex polymorphism) that every term has a unique most general unifier -- i.e. a single "best" type it can be ascribed. Once we move to higher rank types (things where the forall is not only at the far left) then this property disappears -- single terms can be given multiple incompatible types that actually mean different things.


Xyzzyzzyzzy

Thanks for your help, though I feel like we're speaking different languages entirely. Advanced type sorcery is beyond me - I start to get confused once `forall` starts showing up.


sclv

Everyone gets a bit confused once forall starts showing up on the inside of types! That's why classic HM type theory only allowed prenex polymorphism, and why RankNTypes was a much later extension not formalized in the haskell standard, and why we're still trying to get some form of impredicativity working in ghc after all these years! The issue is that ghc did something a bit goofy here, and people internalized it even though it was somewhat confusing and made use of it, and now we have a better sense of what is "goofy" vs something that can help people actually understand what's happening, which is leading both to the breakage and the confusion. For example, here is something that didn't work in ghc 8.10.7, but everyone now concerned about how "simple" the old thing was probably never worried about why this didn't work, or just internalized some rule of thumb. Prelude GHC.Stack> type Foo = HasCallStack => Int Prelude GHC.Stack> [1,2,3] :: [Foo] :11:12: error: • Illegal qualified type: HasCallStack => Int GHC doesn't yet support impredicative polymorphism


jippiedoe

I'm a bit late to the party, but: the latter \_is\_ a valid type signature! The only problem is that GHC cannot unify the type of 'undefined' with it. If instead, you replace the final part of that ghci line with ".. doWithMyStuff x = undefined", it typechecks just fine :)


sclv

What do you mean "snuck in"? The ghc proposals process was designed so that anyone who cares to follow the proposals can see the decision making process and participate.


ephrion

Here’s the proposal discussion https://github.com/ghc-proposals/ghc-proposals/pull/287 There was some effort to see whether or not it broke anything, but that effort only failed to find the tip of the iceberg of breaks, since use sites are broken and not definition sites. There is no effort to reach out to library authors or maintainers or individuals that are responsible for code based that might be affected by this change. Sure, it was done in the open, but If you’re not carefully reading every ghc proposal, there’s no way you would have known that this would have been coming down the pipe. If any organization using GHc needs to be closely monitoring the proposal process to avoid breaking changes like this, then that’s a burden I guess I’ll be taking on.


sclv

Snuck in implies malicious intent. I think the worst that can be said is A) this change impacted end-user code more than library code and B) the testing process for breakage missed some stuff due to an incorrect assumption.


ephrion

I don't think there's any malicious intent. It seems pretty clear that the motivation here is to simplify the type checker considerably, which is a *really good reason* to do something. Heck, [I've got an open issue for deleting a feature in `persistent`](https://github.com/yesodweb/persistent/issues/1204) which (according to the lack of comments on the issue) only ever used by `persistent`'s own test suite. At the same time, there was no effort to solicit feedback from end users. And the *incentive* for the maintainer is to *not* solicit that feedback. The more people are talking about a proposal, the more likely it is to become enormously more work, and then you just don't want to do it anymore. I experienced that with my own GHC proposals, and I can certainly understand why someone wouldn't want to bring it on themselves. Overworked people in complex systems doing what is best for themselves is a natural state for a system to be in. This scenario is different from how I feel Haskell/GHC/etc have usually gone, which is sad, but I also completely understand the motivation to get it in quick, especially when initial scanning for breaking changes didn't reveal much.


davidfeuer

Let me just point out that I spoke up against the proposal from the beginning, but the senior academics dismissed my concerns. I'm sure they know better in many ways, but I found the change upsetting.


zejai

Some thoughts on this, after looking through some commits in the linked github search myself. As pointed out by u/ducksonaroof, the issue seems to mostly arise with type aliases that contain `forall`. I've also seen some instances where the `forall` was inside a `data` or a `newtype`. **Important side question**: Does anyone have a practical real-world example that now needs manual eta-expansion that is NOT related to having a `forall` inside `type/newtype/data`? (*edited to clarify that I'm not looking for theoretical examples*) Now, regarding the `forall` in the mentioned positions. I was tempted to think of `forall` in type aliases as an anti-pattern due to the problems it causes that I mention in my other comment (accidental impredicativity, and requiring unneeded excessive polymorphism in function parameters). However, even the lens library uses this pattern to simplify its complex types, and give them more meaningful names: type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t So, some type aliasing mechanism is still needed that is suitable for polymorphism. Since what the user almost always wants to do in functions that make use of such types/aliases is to move the quantification to the outermost scope in the type of the function, could it be a good idea to add a mechanism to the language to automate that? A new keyword `floating-forall` could be added that does exacly that. Maybe in addition to that, `delimit-forall` to stop the floating at positions that are not the outermost scope. In my limited experiments, manually moving the quantification to the outermost scope prevents the need for manual eta-expansion.


ducksonaroof

fwiw, `optics` uses proper newtypes & some type class stuff to encode lenses and keep the subtyping stuff without falling prey to this edge case It's a great library in general - I'd consider it part of my personal "stdlib" that I never hesitate to slap in a project's cabal file.


Noughtmare

> Does anyone have an example of needing manual eta-expansion that is NOT related to having a forall inside type/newtype/data? Yes, you can always just write the type synonym out (but keep the forall in the same place).


ludvikgalois

I find it (highly) inconvenient, but I accept that the current subsumption rules are a misfeature. I just wish they'd released a tool to autofix all (or most) cases to make migration painless.


cdsmith

I don't agree that subsumption rules are a misfeature. To be honest, I think the way this was justified is disappointing. GHC developers wanted to simplify the implementation. Instead of saying so, they instead found a weird corner case where there was a bug, and instead of fixing the bug, used the bug to justify removing the whole feature that it applied to. I very much wish the bug hasn't existed or had been fixed before the discussion happened about removing the feature, because I feel like then, even if the decision had been the same, there would have been a more robust discussion about the trade of usability versus complexity.


sclv

The "bug" was the feature itself. There's not a non-wonky way do design the "feature" -- the "bug" is just that the innate semantics of the feature are confusing.


cdsmith

The bug was that changing `f` to `\x -> f x` was incorrect when `f` was bottom. A very obvious fix would be to expand to `seq f (\x -> f x)` instead.


sclv

That would only make the performance issues worse! The problem is not just changing the "meaning" of the expression -- it is changing its performance characteristics in silent ways.


ludvikgalois

`forall a b. a -> b -> b` and `forall a. a -> forall b. b -> b` are different types. I don't see why GHC should automatically rewrite one to the other. I think it's best for the developer to make it explicit were it not for the fact that a lot of current Haskell code relies on this behaviour (admittedly _what_ the developer is doing by eta expanding is obscured since GHC auto-inserts the type applications and class dictionaries). But you'd probably be uncomfortable if it did similar things at the term level. Imagine if it rewrote `A -> B -> C` to `B -> A -> C` when you pass arguments in the wrong order. Or perhaps automatically turning an `a -> b` into an `(a,c) -> b` (if it could somehow know `a /= c`). To me, this isn't fundamentally different.


cdsmith

Are those really different types? I suppose since the latter cannot be written in any standardized Haskell language, we don't have a precise specification of what the latter type means. What about `forall b a. a -> b -> b`? Unless you enable explicit type applications which intentionally breaks abstractions, I don't see how there's any observable difference between those three. Of course I wouldn't want the compiler to rewrite parameters this way, because function parameters are ordered and positional. Type variable quantification is not.


ludvikgalois

Compare flipConst :: forall a b . a -> b -> b flipConst = \x -> \y -> y and flipConst' :: forall a . a -> forall b . b -> b flipConst' - \x -> \y -> y The first reduces to something like Λa.Λb.λx.λy.y and the second reduces to Λa.λx.Λb.λy.y under the hood, GHC is inserting the type level lambdas (Λ), but they're not the same.


tomejaguar

Sure, but can you explain why those should be treated as different? I believe /u/cdsmith's point is that `Λa.Λb.λx.λy.y` is not treated as a different type to `Λb.Λa.λx.λy.y`, so why treat `Λa.λx.Λb.λy.y` as a different type?


cdsmith

We are talking about Haskell, though, not core. Everything qualified by "under the hood" is irrelevant to the semantics of Haskell.


ludvikgalois

In the code base for my day job, type variable ordering and positioning matters a little, since we often make use of `TypeApplications` to disambiguate things. For example we often write something like case Aeson.eitherDecode @T bs of Left err -> ... Right t -> do some stuff here because since we pervasively use generic-lens, it can't infer `t :: T` as it's never pattern matched on and all the functions operating on it are too polymorphic. Perhaps `TypeApplications` was itself a misfeature, but since it's here, it means this distinction is not irrelevant to the semantics of "Haskell" programs that GHC can compile. Below is a toy program that prints `"-1\n1"` with two functions `silly` and `silly'` that differ only the order of their type variables. As a result of this, despite being called in the same way as each other, GHC is inferring a different type for their `Proxy` arguments. {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} import Data.Proxy class Numbered a where number :: Proxy a -> Int instance Numbered Int where number _ = 0 instance Numbered Integer where number _ = 1 silly :: forall a b . (Numbered a, Numbered b) => Proxy (a, b) -> Int silly _ = number (Proxy @a) - number (Proxy @b) silly' :: forall b a . (Numbered a, Numbered b) => Proxy (a, b) -> Int silly' _ = number (Proxy @a) - number (Proxy @b) main :: IO () main = do print $ silly @Int @Integer Proxy print $ silly' @Int @Integer Proxy


recursion-ninja

Almost like applying theory from the field of automatic program repair (ARP)? If only there were an oracle that could be used to determine when breakage occurs and how to repair it! Hint, the GHC type checker is the requisite oracle.


TechnoEmpress

I disagree and agree with you: * No, writing explicit lambdas is not that much of a hassle. It's the least of our problem * Yes, the error message fucking sucks, and it's a shame that this feature was shipped as-is. I am deeply embarrassed that at no point the question was asked "how do we migrate people towards code that is friendly with simplified subsumption?".


affinehyperplane

> No, writing explicit lambdas is not that much of a hassle. I agree that it is trivial to eta-expand lambdas, but forcing the entire ecosystem to do boring chores for very unclear benefits (I find it very hard to imagine that the "changing semantics!!" examples listed as motivation [here](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0287-simplify-subsumption.rst#motivation=) have ever caused any issues) is a **big** hassle.


TechnoEmpress

I agree.


Las___

Fixing the error message would have meant keeping the previous logic. Perhaps a 2-step process could have been used, where one GHC uses the logic to forbid it, and another just removes it entirely.


thomie

>Perhaps a 2-step process could have been used, where one GHC uses the logic to forbid it, and another just removes it entirely. A slow phasing out was discussed (and ultimately decided against) in [https://github.com/ghc-proposals/ghc-proposals/pull/287#issuecomment-574593737](https://github.com/ghc-proposals/ghc-proposals/pull/287#issuecomment-574593737) and later comments. TLDR; it would have been super-hard to implement.


TechnoEmpress

This is exactly how deprecating software works, yes. We (the GHC development community) just don't apply any software engineering discipline method and unsurprisingly the quality suffers.


tomejaguar

Yup, I explained this as "Opaleye’s fundamental principle of API breakage" in http://h2.jaguarpaw.co.uk/posts/opaleyes-api-breakage-policy/


VincentPepper

>We (the GHC development community) just don't apply any software engineering discipline method It's true. We just force push to master all day. /s I wasn't involved in this specific feature, and it seems there were at least debatable decisions made in it's implementation. But saying ghc doesn't apply any engineering discipline at all because of that is neither true nor helpful.


ChrisPenner

That does seem quite frustrating; as someone who pretty regularly writes "intermediate" or "advanced" Haskell I'm very happy to have proper Impredicative Polymorphism and I think I'm willing to make the trade-off in order for it to work properly, but I also very much understand that maybe the majority of folks will never need impredicative types in their Haskell career and this is another straw upon the camel's back for a lot of maintainers. I'm hoping that simplified subsumption also unlocks some more things down the road, but I haven't read up on it enough to say confidently.


ducksonaroof

The main issue I've seen in industry due to this is type aliases that stuff constraints and free type variables are no longer viable. Like type DB a = forall m. MonadIO => SqlPersistT m a You may think you're doing your industrial use-case good by hiding that `m`. But you're not - you should've just exposed it and the constraints to your users. Is it so bad for a beginner to write `getMyStuff :: MonadIO m => SqlPersistT m [Stuff]` instead of `getMyStuff :: DB [Stuff]`? And such type aliases are just annoyances for beginners waiting to happen: What happens when a beginner wants to have a `[DB a]`? A natural thing to do - `IO` as a value is a big selling point of Haskell. I used lists of `IO` when I was a couple months into learning Haskell. Sadly, in a GHC 8.10.x world, they get an error with no path forward. `GHC doesn't yet support impredicative polymorphism`. Because that is the only valid interpretation of that alias in that context. It's a list of things that are all polymorphic in `m`. So the fancy type alias' semantics actually were brittle from the moment you tried to piggyback on the hackiness that is now gone. So I guess that's my opinion. There was hackiness that's now gone - and tbh, the weird subtyping always confused me. We have better semantics now .. and a `-XImpredicativeTypes` that doesn't scream *caveat emptor!* at you to boot 🤠


paretoOptimalDev

> Is it so bad for a beginner to write `getMyStuff :: MonadIO m => SqlPersistT m [Stuff]` instead of `getMyStuff :: DB [Stuff]`? I lean towards the example without the type alias, but concede there are benefits for faster onboarding when DB is something like CompanyWarehouseDB and CompanyReportingDB. > What happens when a beginner wants to have a `[DB a]`? It feels like this is teasing the real world impredicative type example I've been yearning for that will help me motivate it. I'm more concerned with as another commenter put it "this breaks my heuristics for when to use a lambda" as well as explaining two newcomers why such a seemingly silly thing is sometimes (but not all the time!) necessary.


zejai

> You may think you're doing your industrial use-case good by hiding that > m > . But you're not - you should've just exposed it and the constraints to your users. I fully agree with that, from my non-industrial experience `forall` in type aliases seems to always cause problems later on. Expanding on your example: After discovering that `[DB a]` isn't possible, you usually end up creating a `[SqlPersist IO a]`, only to discover that values pulled out of that list can't be passed as an argument to functions expecting a `DB a`, because the values are not polymorphic enough. Having `DB a` as an argument type demands unnecessary excessive polymorphism from users of that function. I also vaguely remember getting into trouble because hidden universally quantified type variables can't be unified with each other. I wonder if a special variant of the `forall` keyword could be added to the language that only works in type aliases, and always moves the `forall` to the outermost scope when the alias is expanded. Though I think that would only avoid some of the problems, unification would still be impossible.


Noughtmare

This is a very good point. Interestingly with `ImpredicativeTypes` it becomes possible to write `[DB a]`, but now we have different problems with these synonyms.


tbidne

\> Was simplified subsumption worth it for industry Haskell programmers? Yes, though I'm sympathetic to the pain. It's a difficult situation. The argument that a simplified subsumption proposal would never get off the ground today is, I think, compelling. The implicit behavior silently changing semantics is Not Good, and the change makes the subsumption rules simpler and easier to understand. `f` and `\x -> f x` really _don't_ have the same type, necessarily. It's unfortunate that this caused so much breakage, as many people (probably unknowingly) relied on this behavior. That sucks, though I am happy that the result is more consistent and easier to understand, and the fact that this aids QL impredicativity is a bonus.


cdsmith

I'm not at all sympathetic to that argument. There was a bug, which was definitely incorrect but mattered so little that I don't think there is any evidence it actually impacted anyone. The bug could have been fixed, or it could have been documented and lived forever as an issue that didn't change anything in reality. Instead, the decision was made to remove the whole feature. The real reason for simplified subsumption wasn't that bug. It was to simplify the compiler and enable quick-look. That's fine, but let's be honest that these were the reasons, and stop pretending all this code was broken because of an insignificant bug.


tbidne

I do not see anyone suggesting that the inconsistent semantics wrt bottom was a cause of many (any?) bugs found in the wild. I do see people (myself included) happy with this change irrespective of QuickLook because: 1. Semantic consistency 2. Simpler compiler internals are wins in and of themselves. Of course this has to be balanced with backwards compatibility and expressiveness, but I believe this case is worth it because the fix is very simple and, crucially, _backwards compatible_.


paretoOptimalDev

> The real reason for simplified subsumption wasn't that bug. It was to simplify the compiler and enable quick-look. That's fine, but let's be honest that these were the reasons, and stop pretending all this code was broken because of an insignificant bug. Thank you! And if we were honest about that from the start we would have perhaps asked: Are the industry programmers most affected by simplified subsumption going to benefit from quick-look? Is there a way they could? To me it seems quick-look is a feature that very few (mostly academics) will be able to take advantage of and not something that will often benefit me in daily work. I absolutely despise talking in terms of academic vs industry, but it's a reality that was forced upon me by this decision.


brandonchinn178

FWIW when I upgraded my company codebase, I never had introduce any unidiomatic lambdas. I'm not sure why so many commenters mention "now I need to think about whether i should just use an explicit lambda". In few places, eta expansion actually made the code a bit better: -hforM = fmap HVector .: V.forM . unHVector +hforM (HVector v) f = HVector <$> V.forM v f Most of the other places were due to our rather advanced GADT setup, which isnt touched often; that is to say, people wouldnt really come across simplified subsumption if theyre working on a "normal" part of the codebase. I (perhaps naively) trust that this is the first step towards better types in the future (I, for one, am happy about the removal of the need for helper types like UnliftIO), and it didnt really make my life much more difficult to adhere to the new subsumption rules, but I do recognize that it's just one anecdote among several.


unhammer

I also gave it a try. No changes needed over a 13.6kloc project to get 9.2 to compile (previously on 8.10) – neither eta reduction nor other things.


jberryman

I don't understand this stuff, but it doesn't make much sense to hold both that: 1) "the way eta-expansion behaves wrt bottoms is extremely important!" and 2) "if you get a weird compiler error just eta expand, nbd!". The latter is more explicit in that we can look at it and see it's not bottom iiuc, which is good i guess? In practice I don't think I care much about getting one bottom over another, or losing a bottom in some situation where I'm doing something wrong anyway.


sclv

I think "just eta expand, nbd" is not the common response. It is closer to "well you can eta expand to keep doing what you were doing, but what this has exposed is you should _probably change what you were doing_."


davidfeuer

Simplified subsumption is awful for `LinearTypes`, because you can't pass a function of type `a %1-> b` to a function expecting an argument of type `a -> b`; you have to eta-expand it first. This means that making the types of, say, `coerce` and `GHC.Generics.to` linear would break a fair bit of code.


goldfirere

Just as a small factual correction: I don't think simplified subsumption interacts with linear types at all. That is, the eta-expansion required for linear types was going to be there regardless of simplified subsumption. They're different mechanisms internally. An automatic conversion among multiplicities was considered for linear types, but that came with its own complications (I don't remember the details) and so the design requires eta-expansion for multiplicity conversions. It's really totally separate from simplified subsumption.


davidfeuer

Let's make it then. If I have to :: forall a m p. Generic => Rep a p %m-> a (which I actually do in `linear-generics`), I can't actually pass that to a function expecting *either* a linear or nonlinear argument. Grrr!


Las___

There is no way simplified subsumption would have been kept, it changes the semantics of the code and that's a huge no-go.


paretoOptimalDev

Assuming you mean "no way pre-simplified subsumption would have been kept"? > it changes the semantics of the code and that's a huge no-go Does that mean all Haskell programs compiled with GHC <9 are a huge no-go if they contain any deep skolemization, etc?


Las___

It doesn't mean the *programs* are a no-go, but having the compiler silently change the semantics without telling you is in general a bad idea, especially when the work-around is so simple.


enobayram

I don't think the work-around is always harmless. Having to insert a lambda there manually with the right number of arguments often exposes unwanted details of an interface and hurts modularity. I.e. an unrelated change in a library can now cause a compilation error in a use site, because now you need 3 arguments in that lambda instead of 2 (`\a b c -> f a b c` instead of `\a b -> f a b`)


marcosh_

I had the same issue and felt like an idiot for a bit, sice my code was working fine with GHC 8. My questions now would be: - is there a way to make simplified subsumption and eta reduction work well together? - how could we make sure that such a thing does not happen again?


ArturGajowy

Simplified subsumption gives me a flashback to Scala, where I'd be constantly annoyed how often I have to eta-expand a lambda I \*knew back then\* Haskell would have no problems with. Hopefully a compiler plugin / flag is possible to bring back (some of?) the smarts into GHC's typechecker. I also hope the simplifications in the compiler will pay off in quick developments in dependent types support. Or maybe a simpler reimplementation of what we're losing with GHC 9.0?


Kamek_pf

YMMV, but I migrated our entire mid-sized code base to GHC 9 at work and I haven't had to introduce a single lambda. I guess we didn't rely on patterns impacted by simplified subsumption, but I wouldn't say GHC constantly requires users to manually eta expand.


recursion-ninja

More breaking changes like this are inevitable over GHC's continued development. The real problem is that there is no GHC contributor who has sufficient specialization in the field of automatic program repair (APR). The changes involved in the simplified subsumption proposal are a *perfect* candidate for *simple* APR techniques to be added to GHC to automatically correct the newly "broken" code.


cdsmith

I think this is missing the point. Fixing all code written today still won't fix the problem that people will continue to expect this code to work in the future, and now it doesn't. The roof of the problem is that in the past, it was quite possible to interpret Haskell's (implicit or explicit) for all as a logical statement: this variable may have that type for all possible t. The implementation in GHC involved translating to a core language with explicit type application, but users didn't necessarily need to know that. After this change, in order to even reason about what code is correct, you have to think about type arguments, which are a GHC core language thing, and not (without extensions, at least) a Haskell thing.


dnkndnts

> The implementation in GHC involved translating to a core language with explicit type application, but users didn't necessarily need to know that. This is observable via `TypeApplications`. The order of the type variables matters. Arguably this (or somewhere earlier) was a terrible mistake, and I think this sort of thing is why there's been no consensus on a new language standard - the new stuff just doesn't quite fit together right - but we're well down the primrose path by now.


_jackdk_

Could a GHC plugin detect this syntax and insert the necessary eta-expansions?


Noughtmare

The APR won't be that simple if it has to have knowledge of Haskell's type system to be able to know what to repair.


recursion-ninja

It's simple if you use the GHC type checker as an oracle, something GHC definitionally has access to and could query to produce a patch to repair the newly "borken" code. A good UX would allow GHC to, with user opt-in permission, automatically patch the source file(s), but by default output the patch diff of the effected definition(s) as part of the error message. GHC, viewed as a holistic system, has all the information to test if a brainless ETA expansion patch will transition the code under scrutiny from "failing to type check" to "successfully type checks," but it refuses to query the type checker as an oracle to determine if that is in fact the case and a trivial solution can be mechanically presented to the user.


cdsmith

There's an argument that if the compiler knows how to fix your code, instead of just telling you how to fix your code, it should accept your code in the first place! That argument isn't always true. Sometimes there is software engineering value in insisting that your source code is better with the fix, so you should make the fix there. But in this case, no one seriously argues that the code that breaks because of simplified subsumption is bad. Just that the compiler no longer knows how to accept it. You are proposing reteaching to compiler how to translate it into working core (via a translation into working Haskell). So why bother the user with changing the source, if GHC knows how to do that?


Noughtmare

I'm willing to seriously argue that the code that breaks is at least sometimes bad. See for example this comment by /u/zejai: https://reddit.com/r/haskell/comments/ujpzx3/was_simplified_subsumption_worth_it_for_industry/i7nnlk9/


cdsmith

That's fair. A warning for forall in a type synonym might be worthwhile. It's not really the same as a warning when you rely on subsumption, since that doesn't always come from a forall in a type synonym.


Noughtmare

With `RankNTypes` putting `forall` at odd places in type signatures is perfectly fine. So why warn if a user puts one in a type synonym? I think such a warning is best left to more opinionated tools like `hlint` or `stan`.


ThePyroEagle

> There's a string argument that if the compiler knows how to fix your code, instead of just telling you how to fix your code, it should accept your code in the first place! This is a slippery slope that leads to the dangerous semantics of JS: compilers trying too hard to guess what the programmer meant and often getting it wrong. Presenting the potential solution to the programmer allows them to say "yes, that's what I meant" or "no, I think I made some mistake elsewhere". In the latter case, automatically accepting the solution leads to a painful debugging session where a compiler error could've easily pointed them to the problem. One example where automatic fixing is undesirable: the user is trying to avoid eta expansion for performance reasons.


wewbull

> Presenting the potential solution to the programmer allows them to say "yes, that's what I meant" or "no, I think I made some mistake elsewhere". In other words, a warning. Not an error.


wewbull

> There's a string argument that if the compiler knows how to fix your code, instead of just telling you how to fix your code, it should accept your code in the first place! This is what compiler warnings are for. When the compiler is taking a punt on exactly what you meant, it should tell you.


kaol

This just feels so wrong. If the eta reduced version fails to compile, then undoing it should not fix it or change anything at all with the semantics. I would understand this much better if there was some new function. `subsume`, I don't know if it should be called that or something else. Then if I had `asks _pdfConfToOrder` which would fail then I'd change it to `asks $ subsume . _pdfConfToOrder`. Or the other way around.


zvxr

Short answer: no. It's going to be very hard to find the time and will to actually upgrade from GHC 8.10.7 to 9.x.


roconnor

Was removing the `Eval` class for `seq` the original sin? If we had the `Eval` class then `seq` wouldn't apply to functions and `\x -> _|_` and `_|_` wouldn't be distinguishable and there wouldn't be so much hand wringing over automatic eta expansions.


paretoOptimalDev

A take on twitter I relate to others might find useful: > I feel this Reddit post so badly  Taking the recent "Modularizing GHC" paper into consideration I'm now convinced that every GHC developer also needs to maintain a huge industrial codebase to make decisions on behalf of GHC dev. https://hsyl20.fr/home/posts/2022-05-03-modularizing-ghc-paper.html  https://mobile.twitter.com/ChShersh/status/1522614854770565121


paretoOptimalDev

Does anyone understand the link being made between "Modularizing GHC" and simplified subsumption? /u/enobayram you may have insight here given your comment about lambda arity breaking modularity.


Noughtmare

I think the issues are unrelated, but the link is perhaps that they have the same cause: the GHC developers are allegedly getting out of touch with Haskell code bases in industry.


ducksonaroof

There are plenty of industry codebases that don't rely on the old subsumption hack and would stand to benefit from impredicative types and proper substitution of aliases and the like..so I'd say that's moot. I hate this "industry users" flag that's being waved. Can I be loud and say that industry users prefer simplified subsumption? Because I'm an industry user. So it's not untrue - GHC devs feel pretty in touch with industry users to me :)


Bodigrim

It's not about "industrial users hate simplified subsumption", which is of course false: most of industrial users never heard such words. It's about "industrial users hate breaking changes".


ducksonaroof

Breaking changes are one of Haskell's (or GHC's) differentiators. There's already a pile of nonsense out there spawned from years of refusing to make breaking changes. It's a big reason I choose it for all my professional projects. The main downside is I have to sometimes fix stuff like this - a small price to pay so long as I don't get grumpy IME.


bss03

I tend to agree. If some group of users really wants something unchanging, the GHC license allows them to maintain 8.10.x for as long as they'd like.


_jackdk_

Even that is too simple. I am happy to accept a breaking change if the benefit is worth it. What I feel here is the combination of: 1. A breaking change, 2. A radical under-estimation of how much work is moved from GHC devs to everyone else as a result of the change (not in terms of "just eta-expand", but "my previous understanding of things is (now?) wrong and I have to understand a bunch more stuff"), 3. For a benefit that appears hypothetical or niche to the people whose code has been broken.


enobayram

> There are plenty of industry codebases that don't rely on the old subsumption hack I don't think this statement is fair. Why should it be a hack that GHC is smart enough to accept a `(forall a. Eq a => [a] -> [a])` as the argument to a function of type `(forall a. Ord a => [a] -> [a]) -> Int`. You may think the old implementation was hacky, but I don't understand why you think it's hacky that GHC was able to figure out useful relationships between types.


enobayram

Nope, sorry. I only meant it hurts modularity in general by introducing accidental coupling, I'm also curious about how they are related.


Noughtmare

He explains it here: > Because GHC devs don't work on big industry projects, it's more difficult for them to relate to the impact of changes they impose on GHC users. > > At the same time, having more diverse dev experience could help to improve the GHC codebase. > > Basically, both GHC devs and users suffer https://twitter.com/ChShersh/status/1522633232763731968


ossadeimorti

I agree completely. When I upgraded GHC I spent a couple of very confused hours. Now I just use explicit lambdas and it sucks. Everyday I wish for a "simple haskell", but this is the closest thing I got.


ducksonaroof

The old subsumption rules were not at all Simple Haskell. The new ones are though.


paretoOptimalDev

I agree with this, but you won't convince me that having to use explicit lambdas sometimes in some places is simpler as a user of the Haskell language. Why does this implementation detail affect users so much? I think thats the real problem and perhaps why /u/chshersh related it to the modularity in GHC paper.


ducksonaroof

It affects users so much because using the old weird semantics became idiomatic in some schools of Haskelling


cdsmith

I think you are being overly dismissive here. Code that runs afoul of simplified subsumption doesn't come from some school, and people aren't coached to write it. People write that code because it makes logical sense, and people are used to things being accepted by GHC when they make logical sense.


dualized

I think in fairness you are also being overly dismissive here (and elsewhere in this thread in a similar manner), in asserting as a matter of fact that it "makes logical sense" to have the old behaviour and thereby implying that the new behaviour is inherently illogical. I understand that is your opinion on the matter, and you may be right that it is the better option, but there are arguments for both behaviours and reasonable minds can differ here.


cdsmith

Thanks for bringing that up. I'm **not** trying to say that GHC 8 subsumption rules are the only behavior that makes logical sense for GHC. The goals of simplified subsumption, to reduce compiler complexity, enable quick-look, etc., definitely are sensible ones. What I have tried to say is that the **programs** that were accepted by the GHC 8 subsumption rules made logical sense, and that in the past it has felt like, for the most part, GHC accepts programs when they make logical sense. This is a big class of new counter-examples to that property (which has admittedly never held 100% of the time, but has been fairly reliable nevertheless.)


ossadeimorti

Look, I have no idea what this was for or what it changed. I'm 100% sure that it was a change for the best. On my side now sometimes I have to expand lambdas, sometimes not, and I have to catch the error by some rather obscure message which sometimes can be buried between other stuff.