10 ms·

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

103 points by setra 8y ago

dustingetz 8y 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?
- lmm 8y 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 8y 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!
- marcosdumay 8y 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 8y 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 https://wiki.haskell.org/Bottom
- d_ 8y ago
  Most functions we write are indeed total.
- klodolph 8y 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 8y ago
    Can you give a practical example of such nonterminating subexpressions?
- dustingetz 8y 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-language-for-super.html 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___ 8y 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).
lmm 8y 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 8y 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.
  - lmm 8y 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).
    - yvdriess 8y ago
      I would say 'by-demand lazy' failed. The by-demand implementation gives a guarantee that an expression is never evaluated if it is not used. Other non-strict forms exist where every expression will be touched, but no guarantees are given on the ordering. MIT's pH Haskell dialect is an example of this.
danabrams 8y ago
The real monad was the friends we made along the way.

103 points by setra 8y 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?

lmm 8y 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 8y 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!

marcosdumay 8y 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 8y 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 https://wiki.haskell.org/Bottom

d_ 8y ago
Most functions we write are indeed total.
klodolph 8y 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 8y ago
  Can you give a practical example of such nonterminating subexpressions?
dustingetz 8y 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-language-for-super.html 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___ 8y 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).

lmm 8y 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 8y 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.
- lmm 8y 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).
  - yvdriess 8y ago
    I would say 'by-demand lazy' failed. The by-demand implementation gives a guarantee that an expression is never evaluated if it is not used. Other non-strict forms exist where every expression will be touched, but no guarantees are given on the ordering. MIT's pH Haskell dialect is an example of this.

danabrams 8y ago

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