4 ms·
No. 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 existin
by anderskaseorg 5y ago
No. 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.