Haskell - Does "IO ( )" means we give up the control of our program?

Question

We know that within a Haskell program, almost every piece of computation will return something, and such return values can be captured by another computation to apply more transformations on it. So if we "flatten" a normal Haskell program, it should be:

-- pure `a`: comes from Hask; not from file, network or any 
-- other side-effected devices

a → a' → a'' → a''' → .... → a_fin

Of course, this pure value might be "contexted". But we can still trace the path of alternating:

a → m a → m a' → a'' → n a''' → ... → z a_fin

For me, this shows that we can control our program to avoid side-effects and other 'surprises', which may be caused by missing of type system or our self. But when the IO () appears, there seems a missing:

--!! What happened between the IO () and the next computation ?

a → m a → m a' → IO () >> b → b' → m b'  

The IO () seems passing/receiving nothing, but it MUST read/write something at least. Especially if we consider the "receiver" process:

Sender::   a → m a → m a' → IO () >> b → b' → m b' ... → m b_fin
Receiver:: IO a' → IO a'' → IO a''' → ... → IO a_fin

In the sender, we can't see what happened on a after the IO () . But if we consider both two processes , the missing part is back ! So we can say we missed or not missed the information, according to your point of view. Is this a information leak, and we just give up the control of our program, when we put the IO () in the program ?

Thanks !

PS. Oh,and I also found that the Receiver, can only start computation with a "contexted" value, not a pure value, it's another question occurs in my mind...

Answer 1

Yes, from a certain point of view values of type IO a pull information out of thin air; information that doesn't originate in the inputs to the function that produced them. That's inevitable, as the entire point of IO is to write computations whose results depend on (and can effect) the world outside the program. The information that results from a call to readFile resides in a file on disk, not in your program. So yes, you're "giving up control" in the sense that the results of any program using any IO action depend on thing that are not under the control of the program you're writing. But every program is like this; the only way to avoid it is to not use IO (or any mechanism of communicating with the outside world) at all, and then your program is just an extraordinarily complicated way of writing down whatever the final result is.

But the type system never cares about the actual intput/output values, and it doesn't prove that they are correct, even when IO is not involved. In type checking a function of type Integer -> String all it does is verify that it is implemented with operations that will indeed accept an Integer and return a String. It has no conception of whether the correct string is produced.

You can even "lie" to the type system; undefined is a valid definition for any function, which then gives you a function that e.g. takes an Integer and returns a String as far as the type system is concerned. But that doesn't mean it's a correct implementation of that function; and any other function defined in terms of this one will be incorrect too, and the type checker doesn't care at all.

Likewise, a function of type Integer -> IO () checks that the function uses operations that accept an Integer and produce an IO (). That's all that type checking proves, and this is no different for IO () than for IO Integer or for Integer, or any other type.

Answer 2

IO () means that the computation may be influenced both by past IO actions, and that it may influence future IO actions in your "computation chain". However, non-IO values (anything that, if it has a monad stack, does not have IO anywhere in the stack) that follow cannot be directly affected, since () is the trivial value, and that is all they are allowed to depend on. They can be indirectly affected if they depend on some IO a that is affected. This is ignoring unsafePerformIO, which should only be used in such a way that the above explanation still essentially holds true.

Answer 3

From your comments it looks like that you think that because IO ()-typed computation does not return something useful the type system cannot guarantee that your program is correct.

First, the type system does not guarantee correctness of your program except in simple cases. In complex programs it is entirely possible to make logical mistake and your program will compile but return wrong results. It is programmer's duty to avoid logical errors, and type system is only one (powerful one indeed) tool.

Second point follows from the first. IO is a plain monad; it is the same type (from the point of view of type system, of course) as any other. AFAIK it does not receive some special treatment from the type system. The value of type IO () does mean 'an impure computation which, when executed, may affect outside world in some way and which does not yield anything meaningful' and nothing more. Consider value of type State Int (): it means 'a stateful computation which, when executed, may do something with current state of type Int and which does not yield anything useful'. You see, both of these values have some kind of side effect and both of them has the same meaning related to computation result. They are equivalent in this way from the view of type system. But the second one is perfectly pure computation. You easily can turn it to some meaningful value (in this case, Int) using execState or runState.

Answer 4

No. You're thinking that each action in the chain can only see the result of its immediate predecessor; but in reality, each action has access, if it wants, to the result of any previous action. Just to use a toy example:

return 5 >>= (\x -> putStrLn "mwahaha!" >>= (\_ -> putStrLn "x is " ++ show x >>= (\_ -> return ())))

Note the scope of the variable x—it extends to the end of the whole expression. (The parentheses are optional there, but I put them in to make the scope obvious.)

Consider again the type of >>=:

(>>=) :: Monad m => m a -> (a -> m b) -> m b

This can be paraphrases "use the result of an action of type m a and a function of type a -> m b to construct the rest of the program" (not just the next action).

Actions also have context to mutable memory and any I/O device available to the program, so that's also another mechanism by which an action can communicate with another. Two actions of type IO (), for all you know, can communicate through shared memory or by sharing a file.

Answer 5

I'm not quite sure what the question is, but I'll throw in an answer in the case my intuition is correct, anyhow.

The fact of the matter is that, if you were to solely look at the type of the program's constituent functions, you can come to one of two conclusions:

1. Your program does not use IO, and the computations are therefore guaranteed to be pure, and thus produce no side-effects(Within certain limits, of course.)

or

1. Your program does use IO, and is therefore not pure, and it cannot be guaranteed that it does not produce side-effects.

Of course, there are computations within the spectrum of all possible IO computations that produce no side-effects, just as there are computations whose types indicate purity, but use unsafe functions such as unsafePerformIO. But in general, you can look at the type of a pure function and say: This function will not fail on disk IO, network IO or anything of the sorts. That same guarantee does not hold for IO computations.

Answer 6

This chain consists of “states” of your program (well, sort of). Let’s consider a simple program:

main = do
  let a = 4  -- 1
  print a    -- 2
  print a    -- 3

Here, after step 1 your state is 4. But after step 2 this 4 doesn’t disappear — your state now is (4, ()). After step 3 it is (4, (), ()) and so on.

---

To make long story short, information which will be used later remains in the chain. It doesn’t disappear after IO ().