Is this a reasonable view of Haskell IO?

Question

Is this a reasonable view of Haskell IO?

When given a program, the Haskell runtime does the following:

1. Calls main to get back an "IO computation"
2. It then executes or "runs" that computation thereby performing all of the side-effects the computation contains.

This two-stage approach allows main to remain a pure function.

An IO computation in this case is like a special version of Haskell that has explicit sequencing - or perhaps there is a better way to describe this?

Answer 1

Yeah, that's a decent semantic model of how the programs are executed. The implementation doesn't work like that, of course, but you can still use that model to reason about the programs.

But more generally, what IO does is to allow you to treat imperative programs as pure values. The Monad operations then allow you to compose imperative programs from smaller imperative programs (or to use the usual term in this context, actions) and pure functions. So the purely functional model, while it cannot execute imperative programs, can still describe them as expressions of type IO a, and the compiler can translate these descriptions into imperative code.

Or you could say this:

• The compiler (not the runtime) evaluates main.
• The result of that evaluation is an imperative program.
• This program is saved to the target executable.
• You then execute the target program.

I.e., the "evaluate main" part of your model is pushed to the compiler, and is not in the runtime as you first describe it.

Answer 2

Your view of IO is good, but I have a problem with this line

Calls main to get back an "IO computation"

The best way to think about Haskell is that functions dont do anything. Rather, you declaratively describe what values are. A program consists of a description of an IO value called main. The only sense to which it "calls main" is that the declaration of main is reduced to Weak Head Normal Form (or something similar).

IO is the type of arbitrary side effect-full computations. The pure subset of Haskell is a purely declarative description of values, that happens to allow for undecidable descriptions. Think of Haskell as a mathematical language like set theory. Statements in set theory dont do anything, but they might involve complicated computations like "the smallest set which contains Akerman's_function(30)". They can also contain undecidable statements like "S = the set of all sets that do not contain themselves"

@amindfv is half right: main is not a "pure function". It is not a function at all. It is a value, defined by a pure reduction, encoding unpure computation.