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

http://www.cse.chalmers.se/~nicsma/no-state-monad.html

by setra • 8 years ago

103 69 8 years ago

cse.chalmers.se

dustingetz3• 8 years ago

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?

lmm16• 8 years ago

It seems to me a piece of software is either a formal proof or it's not.

That seems like a false dichotomy. Rather I'd say: a program carries a bundle of proven properties with it, but for some programs this will be rich and for others it will be more or less trivial.

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?

To what degree do we actually write robust programs though? Errors are so common we dismiss them and retry or work around without even consciously noticing the error. "Have you tried turning it off and on again" is funny because it's true.

carterschonwald• 8 years ago

This is all pretty fun reading.

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).

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.

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!

marcosdumay2• 8 years ago

This.

This thing is not a problem on Haskell because everybody always code defensively against bottoms. GHC is quick to teach this to novices.

It may still be a problem of "the lack of this feature inviabilises a lot of good code". It doesn't look like it is, but nobody can be certain, so it's a good avenue to explore.

pacala• 8 years ago

Cute, but why should one care about ⊥, aka bottom, aka nontermination [0]? Let's write programs that terminate...

[0] https://wiki.haskell.org/Bottom

d_• 8 years ago

Most functions we write are indeed total.

klodolph• 8 years ago

We care deeply about ⊥ because in our terminating programs there are often sub-expressions that do not terminate. Without ⊥, we cannot reason effectively about Haskell.

You can require that all of your functions are total and still end up caring about ⊥.

catamorphismic• 8 years ago

Can you give a practical example of such nonterminating subexpressions?

dustingetz3• 8 years ago

Proof of termination is closely related to :

"Now suppose there were a hypothetical language with a stronger guarantee: if two programs are equal then they generate identical executables. Such a language would be immune to abstraction: no matter how many layers of indirection you might add the binary size and runtime performance would be unaffected."

http://www.haskellforall.com/2014/09/morte-intermediate-lang...

A more practical reason to care is that if a user-generated expression is proven to be pure and to terminate, then we can evaluate it without fear of getting hacked, denial of service, etc. Imagine a new type of iphone, IDE or web browser where a shitty app/plugin can't lag up your experience.

g___• 8 years ago

You need more than termination to protect against a denial of service; you need to know that a function terminates promptly. Most denial-of-service attacks are about functions that run slowly (e.g. O(N^2) or exponential).

lmm16• 8 years ago

A more practical reason to care is that if a user-generated expression is proven to be pure and to terminate, then we can evaluate it without fear of getting hacked, denial of service, etc. Imagine a new type of iphone, IDE or web browser where a shitty app/plugin can't lag up your experience.

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.

Kutta• 8 years ago

no matter how many layers of indirection you might add the binary size and runtime performance would be unaffected

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.

OtterCoder• 8 years ago

It's kind of funny, looking at these halting discussions as a backend web programmer. At the heart of it, all I do all day is try to write nonterminating programs in an environment where the entire universe seems hell bent on terminating the event/polling loop. It's kind of perverse when you think about it.

ben5093• 8 years ago

That's why I love containers... you definitely write your code to not leak resources, but if there's any unexpected state, your recovery strategy is to report the error, bail, and the whole container is blown away.

Zalastax• 8 years ago

The nice thing is that you can actually build stuff like web servers in a total language :) Using something called co-induction a total language can model things that are potentially infinite, e.g. a web server. Co-induction replaces the requirement that every function must terminate with the requirement that the next step (e.g. the next value of a stream) can be calculated in finite time. So, the event loop could be modelled using co-induction as long as long as the event handlers do not contain infinite loops.

dustingetz3• 8 years ago

Modern/future serverless paradigm models services as functions for example https://docs.datomic.com/cloud/ions/ions.html

geofft• 8 years ago

The usual argument given for wanting programs to halt is that if you can't solve the halting problem for your language you can't prove anything, so we want languages where we can prove things.

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.

marcosdumay2• 8 years ago

The web is completely transactional. You want nearly all your code to terminate (and fast), it's just some small layer that will call the terminating part that you want to run forever.

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.

lmm16• 8 years ago

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.

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 if two expressions are equivalent-up-to-⊥. and both non-⊥ then they are equivalent.

(Or, y'know, work in Idris with --total and avoid this problem entirely).

dwohnitmok• 8 years ago

Just to agree and emphasize, a more accurate title would probably be "Breaking eta equality breaks the monad laws." A lot of equational reasoning in general goes out the door at that point, not just monads.

More generally any kind of system that is able to introspect and differentiate between non-equivalent evaluations of itself tends to break a lot of invariants.

Imagine trying to establish equivalences between sequential and concurrent processes if the processes in question could introspect what thread it was running on and changed behavior based on that.

So yeah. Seq is what breaks things here. Not State. But even Haskell sometimes has to compromise purity for practicality.

lmm16• 8 years ago

even Haskell sometimes has to compromise purity for practicality.

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).

sametmax6• 8 years ago

I always scares me how little I understand from comments talking about Haskell. Either I'm much more dumb that I though, or the whole community decided that purity beat practicality.

lmm16• 8 years ago

Quite the opposite; the community is very practicality-oriented. There's just a different style of naming things, because things in Haskell tend to be more general. But in most languages any frameworks will introduce their own terminology; comments about the details of (say) React observables are just as incomprehensible if you're not familiar with React.

Filligree• 8 years ago

Eta-conversion is just the statement that having function(x) { f(x) }, in JS, is equivalent to having f. In short, wrapping a function in another function (or removing such a layer) makes no difference.

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.

kazagistar• 8 years ago

You arent "dumb" if you don't known how to play some game or speak some language; you just haven't taken the time to learn it yet.

myWindoonn• 8 years ago

Yeah, but have you ever thought, "Y'know, maybe the fact that we can't reason in Hask but instead have to work in franken-Hask where not everything works as intended," and then thought, "Maybe this is a problem?"

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.

(Also, since somebody's gonna accuse me of not having read "Fast and Loose Reasoning", I absolutely have, and the biggest disappointment is failing to define useful equality on function values as if they were plain values. Might be impossible in Hask, but it's trivial in Pos, the category of posets; maybe Hask isn't a very good category!)

lmm16• 8 years ago

Yeah, but have you ever thought, "Y'know, maybe the fact that we can't reason in Hask but instead have to work in franken-Hask where not everything works as intended," and then thought, "Maybe this is a problem?"

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.

danabrams• 8 years ago

The real monad was the friends we made along the way.

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

Related Stories