3 ms·

And 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, whi

And 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 nihilō.

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.

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.