someCode :: IO' ()
someCode = do
PutStrLn "What is your name?"
name <- GetLine
PutStrLn ("Hello, " ++ name ++ "!")
runIO' :: IO' a -> IO a
runIO' (Pure a) = pure a
runIO' (Bind ma f) = runIO' ma >>= runIO' . f
runIO' (PutStrLn s) = putStrLn s
runIO' GetLine = getLine
main :: IO ()
main = runIO' someCode
You might ask, what’s the point of separating it out this way, when obviously you still need to actually perform the effects at some layer? The point is to demonstrate that running code in the IO' monad (and, similarly, the IO monad) does not require “reaching into” the pure functions that define it and violating their purity; you just use them as black-box mathematical functions. All the equational reasoning you can do with pure functions applies equally well to the IO monad.
This is entirely different, for, say, floating point arithmetic, which one could in theory simulate from the ground up by defining one's own float as a vector of binary states and manually implement floating point arithmetic on it.
> All the equational reasoning you can do with pure functions applies equally well to the IO monad.
Only because these primitive functions receive special treatment from the optimizer which ensures that they are not optimized in the same way and allowed to be executed in indeterminate order. — they are very much magical primitives that cannot be simulated ex nihilō.
-- action -> input -> (return, remainingInput, output)
simulateIO' :: IO' a -> [String] -> (a, [String], [String])
simulateIO' (Pure a) input = (a, input, [])
simulateIO' (Bind ma f) input = (b, input'', output ++ output')
where (a, input', output) = simulateIO' ma input
(b, input'', output') = simulateIO' (f a) input'
simulateIO' (PutStrLn s) input = ((), input, [s])
simulateIO' GetLine (line : input) = (line, input, [])
λ> simulateIO' someCode ["Anders"]
((),[],["What is your name?","Hello, Anders!"])
You have described the typological constraints the IO Monad conforms to, but you have not actually implemented any functions in it.
That is why some are of the position that it is merely a type system hack that fools the type system into thinking that it is pure as any other, whereas under the hood it requires coöperation from the optimizer with vacuous dependencies to ensure that all executions happen within the specified order.
The axiomatic functions of the IO Monad have to be provided as primitives by the compiler, they cannot be written as a purely library function, unlike, say `||` in Haskell which can actually be realized as a library function unlike in most languages where it must be a specially treated primitive.