4 ms·
You can write real code given only the definitions I gave: someCode :: IO' () someCode = do PutStrLn "What is your name?" name <- GetLine
by anderskaseorg 5y ago
You can write real code given only the definitions I gave:
someCode :: IO' ()
someCode = do
PutStrLn "What is your name?"
name <- GetLine
PutStrLn ("Hello, " ++ name ++ "!")
and you can run any such program, for example by translating it to the “real” IO:
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
or you can imagine an implementation of Haskell where IO is IO' and PutStrLn really is that data constructor and no such translation is necessary.
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.
- Blikkentrekker 5y agoAnd then you still define them in terms of the actual primitive functions that are a hack. 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ō.
- anderskaseorg 5y agoNo. runIO' does not define PutStrLn, it translates PutStrLn; there’s a difference. I can write and compile all the IO' code I want without runIO' ever existing, and it has the semantics it has as a data structure built from pure functions. I can write a pure function that computes which effects would happen for a given IO' action for a given sequence of inputs, and I can evaluate this function within the GHC REPL. None of this receives any special treatment from the optimizer. -- 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!"]) The fact that the real IO receives special treatment from the GHC optimizer is an implementation detail that’s necessary for the correctness of GHC’s optimizations, but assuming GHC was implemented correctly, this has no visible effect on how programs are evaluated. If you actually run them, the resulting effects should agree with the predictions of the pure function above.