Hacker News Reader

Comment by foldr | Hacker News Reader

The more I've learned about Haskell, the more I've come to realize that Haskell's approach to IO really has very little to do with Monads. Fundamentally, Haskell implementations sequence IO actions using hidden magic. (GHC uses dummy world variables.) As it happens, the operations for constructing IO actions from pure values and for sequencing IO actions form a Monad. But that's not really any more interesting than the fact that e.g. (\x -> [x]) and concatMap form a Monad.

View on HN

This, I feel, is the case with all monads. Even "free monads" are just an interesting name for an AST with embedded host-language functions.

Monad is interesting in retrospect. After you "get" X, Y, and Z you come to realize that they're all monads and then maybe you get some mileage out of the mental compression.

This is a crucial point. There’s almost never value in using any abstraction just once; the value comes when you learn to recognise it and apply previously learned lessons in new situations.

You're describing my pet peeve with research in programming languages, or more generally use of abstractions in CS. What you're writing makes sense: Understand the structure of your problem, then think of similar problems you've seen before, finally try to abstract away details that are irrelevant for the solutions in each case. If you're lucky, all of these problems are an instance of one general one, and need to be solved only once. In your example, it's that IO and [] are both monads and thus share some structure.

What's often happening in PL theory, though, is that people start off with axioms/syntax and then mutilate the actual problem until it fits the syntax (still badly). That's how you get ridiculous stuff like "everything is an object" or "everything is a file". In PL theory, people will usually first make up some syntax/theory and then search for models. If physicists worked the same way, they'd write down random formulae and would then go out to find phenomena described by them. You'd probably read this comment on a cave wall.

Axiomatic formulations of a problem do not have the same goals as abstractions. They can appear similar on the surface, but one has to do with the laying of a foundation and the other is about problem simplification. One is about allowing great leaps in understanding after a great deal of derivation, the other about the reduction of work via problem equivalence. Criticizing someone for using an axiomatic formulation rather than a proper abstraction in programming language theory is like criticizing an architect for using pencil in laying his foundation on paper rather the much more appropriate cement at the construction site.

You don't get everything is an X because of axiomatic formulation. You get it for the same sort of reason that instead of spending ages describing the configurations of atoms in front of you, you throw all that out and call it a screen. Is everything still atoms? Yes! But we can call it a screen and that makes things massively easier to reason about and so we do it, because we like to reason well. But there are still benefits to thinking the other way, thinking from the very foundations. They are just different benefits, which is why we choose to think of problems from more than one perspective.

I didn't mean to critize all axiomatization but the concrete axiomatizations arrived at by PL research. In my opinion, one should start with a thorough understanding of the problem domain, and then try to come up with a syntax that allows expression of your intuition as faithfully as possible. Form follows function. Instead, I feel like PL research is often too focused on the concrete syntax considered, thus function follows form. Case in point: Building models for the syntax at hand is often an afterthought, done only to prove consistency. I'd argue that one should start with as precise an understanding of the intended models as possible, and then come with up with an axiomatization (thus, syntax) for the intended semantics.

For example, the notion of elementary topos has been invented because its creators wanted to capture the way Grothendieck toposes kind of behave like constructive sets. This I find very useful, and also the axiomatizations of elementary toposes. On the other hand, Martin-Löf type theory didn't have a formal semantics at first, then an erroneous one, and finally ~20 years later a kind of acceptable one. And its category of models is... not really interesting. Except for categories of assemblies, I don't know of a single model of ML type theory that's not also an elementary topos. And the interesting thing about assemblies is that they can be turned into objects of the associated topos... so yeah.

And yet MLTT led to Coq, Agda, Idris and Lean, while your ”PL practice” approach sounds like it would lead to, well, Go.

The "everything is an X" is what I call "foundationalism". It is a disease that started with Turing and Church, except that when they started it it was not a disease. But ever since people forgot that Y and "an encoding of Y as X" is not exactly the same thing. For some purposes it might be, but not for all purposes.

Unsurprisingly, Physics get to decide what abstractions they use the same way developers decide what languages to create. They invent some notation, start describing everything they know on that notation, and if it's productive push it further and further until it breaks.

>If physicists worked the same way, they'd write down random formulae and would then go out to find phenomena described by them.

So, String Theory?

Kind of, from what I (complete physics noob) hear.

Reading this: https://wiki.haskell.org/IO_inside did not make me come to that conclusion.

The IO monad is noncommutative, and thus controls sequencing of operations, because of data dependencies, more or less hidden.

A "Haskell wizard" tried to tell me the ordering of operations was implemented through low-level magic a few weeks ago. The fact is that whatever ultimate form GHC might compile your code to, the sequencing is expressible in the semantics of Haskell code. Getting sequencing into the semantics is one of the problems which monads solve.

It's worth noting that the IO monad implementation is very much compiler magic and can't be done in library level haskell. Evaluation order without IO/ST is undefined in Haskell. This is similar to write barriers, you need a magic primop to specify external data dependencies.

Without that magic the compiler may inline everything, drop the 'uselss' state token and happily move your buffer freeing before the allocation - or drop it entirely.

Alternatively you could mark every function as noinline and end up with fantastically slow code.

Data dependencies don't viably smuggle operation sequencing into Haskell. Consider e.g.:

   fma a b c = (a * b) + c

The sum depends on the product but this doesn't sequence anything: it may be compiled into a single fma machine instruction. More generally inlining, CSE, etc. can break apparent data dependencies.

It's simpler and cleaner to merely state that the Haskell runtime is written to execute IO actions in sequence.

The data dependencies in how monads desugar does force the evaluation order, because the result of the first one is passed to the following one and so on and so forth. The desugaring turns each monadic action into a lambda with one argument.

I think that millstone (https://news.ycombinator.com/item?id=17646166 )'s point was that the sense in which desugaring of monads forces evaluation order is the same as the sense in which

    fma a b c = (a * b) + c

forces evaluation order: you need the result of `a * b` in `fma` in order to add `c` to it. One can argue whether both of these, or neither of these, have the evaluation order forced, but I don't think that it is reasonable to argue that one does and the other doesn't. (There is a slight artefact from the fact that addition is commutative, so that it makes no difference whether you compute `c` first and then add `a * b` to it or vice versa, but I think the idea should remain.)

To discuss this properly, you need to consider the evaluation strategy, which is part of the semantics of the language. Strict, lazy, call-by-need: things do get evaluated in a prescribed order, and sequencing using monads (predictably) involves strictness, meaning that a function argument is evaluated before the function.

These details of evaluation order are important to know, and they are not something to be argued about: they are well-specified and the compiler doesn't just casually make lazy code into strict code or vice versa. That would cause chaos. And what instruction set Haskell is being compiled to is totally irrelevant to this level of the language's semantics.

https://en.wikipedia.org/wiki/Evaluation_strategy

>sequencing using monads (predictably) involves strictness,

Sequencing using the IO monad predictably involves strictness. There is nothing in the type of >>= that forces strictness. That is why, for example, you can usefully bind infinite lists in the list monad. So in e.g. [1..] >>= return . (+ 1), the list is not evaluated before the call to (+).

In fact, binding is not strict in the IO monad either (that's why lazy IO works). It's only the special magic world parameter that is, in effect, evaluated strictly.

Yes, monads don't imply strictness.

The idea of using a data dependency to force a certain order of evaluation predates monads and it predates laziness. So it is implemented accordingly, and any hoops that need to be jumped through in the implementation to make it work aren't magic—they are just necessary to express a long-established pattern.

What monads offer is a way of discreetly passing the state from one operation to the next (the State monad is the model for the IO monad). It removes the need for the programmer to think about that aspect of the plumbing, without creating magic elements in the language.

http://okmij.org/ftp/Computation/IO-monad-history.html

>So it is implemented accordingly, and any hoops that need to be jumped through in the implementation to make it work aren't magic—they are just necessary to express a long-established pattern.

The hoops are magic in the sense that they can't be expressed in Haskell 98 or Haskell 2010. A Haskell compiler is perfectly entitled to optimize out any dummy values which aren't used. That includes dummy world variables.

More generally, it simply isn't possible to use data dependencies -- even real data dependencies -- to control the order of side effects. The Haskell standards just don't provide the guarantees necessary to make that workable, for the reasons that millstone gave.

> To discuss this properly, you need to consider the evaluation strategy, which is part of the semantics of the language.

Yes, you are certainly right. I misread and thought incorrectly that the discussion was about whether certain constructs forced data dependencies in any theoretical language, not in the particular language Haskell.

> These details of evaluation order are important to know, and they are not something to be argued about: they are well-specified ….

While I take your meaning, I think that you don't mean literally what you said: they got to be well specified precisely by being argued about, and will hopefully get to be even better specified by continuing argument. They are certainly not for me to argue about, though.

Yes, but there is no guarantee that the argument passed to that lambda will ever be evaluated. Consider e.g. the following expression in the identity monad:

do { x <- return [1..]; return 7 }

That evaluates to 7, and the infinite list is never evaluated. So the 'data dependency' that monadic bind gives you doesn't, in general, force evaluation order. It's only because the implementation details of the IO monad ensure that the dummy world parameter is always 'evaluated' that you get guarantees about evaluation order. Note that the dummy world parameter is just that -- a dummy -- and no computation actually depends on its value. It's pure compiler magic.

Yep, you can alternatively use unique types (https://en.wikipedia.org/wiki/Uniqueness_type) to do IO while still maintaining referential transparency. Clean, Mercury, and Idris does this.

I’m not sure I follow, since the implementation details of any given monad have very little to do with monads. It’s the fact that IO/Continuations/Etc can be just another monad that was interesting when it was discovered. It’s cleaner to have 1 pattern/framework for N domains than to have N for N.

>since the implementation details of any given monad have very little to do with monads

Well, yes, that's the point. You don't need to understand anything about monads to understand how the implementation of >>= for IO forces the correct order of side effects.

Actually, that is not entirely true. The monad bind operator introduces a data dependency which is responsible for the sequencing itself, not the actual implementation of the bind (i.e. it is a result of the type of the bind).

But I do agree with the general idea that Haskell as a language is still a leaky abstraction, you still need to understand a lot of behind-the-scenes stuff, like how the RTS interacts with the OS ABI, how concurrency is implemented, the consequences of laziness and so on. Just knowing the denotational semantics of the language is not enough.

Ordering of operations is done by the non-associativity and non-commutativity of the bind operation. Data dependency is not sufficient for ordering IO¹².

Well, that's in theory at least. In GHC Haskell the ordering is not denoted by neither data dependency ot the operator semantics, but by a complex set of rules that change from one version of the compiler to the other.

1 - Although it is sufficient for any monad that lacks real-world effects.

2 - Well, technically nothing is enough for really ordering IO operations, but those two properties give single-threaded semantics to IO.

>The monad bind operator introduces a data dependency which is responsible for the sequencing itself, not the actual implementation of the bind (i.e. it is a result of the type of the bind)

No, there is nothing in the type of >>= which guarantees sequencing of side effects. So for example:

a >>= (\b -> c)

There is nothing in the type of >>= that guarantees that a will be completely evaluated before c is evaluated.

I suspect this misconception is what makes many people think that Haskell's way of handling IO has something crucially to do with monads.

I suppose that knowing only denotational semantics would be sufficient only for programs consisting of pure functions. E.g. a batch job that receives input parameters and returns the result via the minimal runtime-provided means would be an example.

It's still useful to understand it a bit deeper to see the similarity between e.g. lists, optionals, and IO.

Well, YMMV, but I don't have any trouble understanding the concept of one thing happening after another without reference to all that other stuff.

I find that kind of comment incredibly misleading. The concepts that most people attach to lists and optionals don't touch functor semantics and thus are miles away from monads.

Saying that lists are an instance of Monad in Haskell says much more about novel ways you can use a list in Haskell than about properties of a monad.

Still, questions like "how do I flatten a list of lists" are common on stackoverflow.

I guess it looked to me like you were singling out IO as a special case, when what you are saying is true of all abstractions. You can just as easily say "you don't have to understand algebraic groups to do integer addition."

As far as I can see, explaining IO in Haskell in terms of monads is unhelpful. It would be like using monads to explain how list concatenation works. The fact that e.g (\x -> [x]) and concatMap form a monad is not really very helpful in understanding what concatMap does.

Reply on news.ycombinator.com