This isn't about the state monad, it's about seq. "But now seq must distinguish ⊥ from λx → ⊥, so they cannot be equal. But they are eta-equivalent. We have lost eta equality!" - once you lose eta equality you lose everything. A whole raft of monads become impossible, not just state.<p>Equivalence in Haskell is defined only up to ⊥; to work in Haskell we rely on the "Fast and Loose Reasoning is Morally Correct" result that <i>if</i> two expressions are equivalent-up-to-⊥. and both non-⊥ then they are equivalent.<p>(Or, y'know, work in Idris with --total and avoid this problem entirely).
This is all pretty fun reading.<p>At least with my own code in Haskell, I work in the mental model where I assume termination and strong normalization (all programs terminate under all evaluation strategies).<p>Then, Bottom corresponds to either an exception that will get forced or a computationally boring infinite loop (which the rts can sometime detect and turn into an exception). My personal style favors having those errors be very very visible.<p>That said, depending on what formal or informal reasoning properties you care about (especially as a library writer), these little subtleties can be really important!
Cute, but why should one care about ⊥, aka bottom, aka nontermination [0]? Let's write programs that terminate...<p>[0] <a href="https://wiki.haskell.org/Bottom" rel="nofollow">https://wiki.haskell.org/Bottom</a>
It seems to me a piece of software is either a formal proof or it's not. So if it's not and we still manage to write robust programs, the natural next question is, to what degree is it okay to knowingly violate the laws? And if you iterate that to the nth, do you end up with Clojure?