Haskell’s State monad is not a monad (2014)

Well, the designers of Haskell made reasonable decisions based on what was known at the time. I'd argue that Idris shows that we don't have to make this particular compromise any more (and, more generally, that the result of Haskell's lazy-by-default experiment is negative).

Like most of lambda calculus, this is extremely intuitive once described that way. Therefore, a situation for which it is false is disconcerting. It's also considered one of the "monad laws", which is the small set of rules that everyone assumes is true for every monad, but which the language doesn't (can't) enforce via the type system.

⊥, pronounced bottom, is a "value" that, if you ask for it, your program breaks. It may go into an infinite loop, or it may crash.

The GP post is therefore explaining that, because eta conversion in this case fails when the function returns bottom, we should be disconcerted. It's a mild form of disconcertion, however: Things would only go wonky if you try to run code that would, in any case, hang or crash.

The reason it isn't completely harmless is that the difference may be observable: A crash in pure code triggers an exception, which can be caught in its impure wrapper code, and a hang can in some cases be converted to an exception by the garbage collector. In theory all bottoms are equal, but in practice they aren't.

In some cases yes. Like I said in my original post, use Idris and then you don't have this particular instance of the problem.

In general though the possibility of failure seems unavoidable; even two runs of a byte-for-byte identical program might "produce different results" if someone dynamites the computer one of them is running on.

> Fast and loose reasoning is not morally correct; it's ethically bankrupt. Programmers in other languages don't get to forget about their errors, imperfections, and footguns; I'm not sure why Hask and Haskell should be let off the hook in our minds.

I don't think there's anything special about Haskell here. Programmers in plenty of languages reason as though exceptions/panics will never happen, and are sometimes surprised by their program's behaviour when they do.

Nontermination alone isn't enough, since in some provably-terminating languages it's still very possible to write expressions that will take a very long time to evaluate in some implementations. Concretely, "catastrophic backtracking" regular expressions can be true regular expressions (and therefore provably terminating), but in naive implementations their runtime will be exponential in the input length.

But it's a start, and the same techniques could hopefully lead to languages in which expressions naturally come with upper bounds on their evaluation time.

This is an unfortunate glaring false statement in the Morte documentation. Correctness of refactoring and code abstraction is understood to be with respect to semantic (extensional) equivalence, while normalization only works up to beta-eta equivalence. It can't eliminate abstraction in general.

Examples in Morte which suggest otherwise use hand-crafted forms of Church-encoded operations which are known to fuse, but there are many equivalent definitions which don't fuse, and which are actually more natural to write. Converting non-fusing definitions to fusing definitions is equivalent to supercompilation, which is generally undecidable, and thus can be implemented only up to some approximation.

But you don't have to have programs halt to solve that. It is a perfectly valid solution to the halting problem that all your event handlers halt and your mainloop doesn't halt (or only halts on receipt of a signal, and never on receipt of a request, or something). And then you have your ability to prove things back.

Thus, you will almost certainly gain by annotating the non-termination at the main loop type, and have the compiler tell you about both any possible bottom at the rest of your code, and any possible termination of the main loop.