6 ms·

It’s easy to demonstrate that the IO monad is pure by reimplementing it in 100% pure code. {-# LANGUAGE GADTs #-} data IO' a where Pure :: a ->

It’s easy to demonstrate that the IO monad is pure by reimplementing it in 100% pure code. {-# LANGUAGE GADTs #-} data IO' a where Pure :: a -> IO' a Bind :: IO' a -> (a -> IO' b) -> IO' b PutStrLn :: String -> IO' () GetLine :: IO' String -- more IO operations… instance Functor IO' where fmap f ma = Bind ma (Pure . f) instance Applicative IO' where pure = Pure mf <*> ma = Bind mf (\f -> Bind ma (Pure . f)) instance Monad IO' where (>>=) = Bind The actual implementation in GHC is much more efficient, of course. GHC does all sorts of magic to hide the fact that it’s generating straight-line code instead of a tree-like data structure full of continuation functions. But it’s semantically equivalent.

Twisol 5y ago
You're right, but I think there's a distinction here that is easy to miss. An IO action describes what to do, but something still has to do that action. A Haskell program on its own doesn't do anything; that's exactly why it's pure. The Haskell runtime interprets an IO value, unraveling it into the string of commands that comprise it. The runtime executes the commands produced by the Haskell program. Haskell uses monads exactly because it lets you describe/express complex sequences of actions (for which later actions depend on earlier actions) without requiring that the machinery for actually performing those actions be part of the program too.
- anderskaseorg 5y ago
  That would be equally true of a programming model where every program is a pure function from a list of input lines to a list of output lines. Everyone would agree that such a model is pure (if limiting), even though the function itself is just a function, and the language runtime takes care of the ugly low-level details of actually making the system calls that read lines from STDIN and write lines to STDOUT. Purity doesn’t mean that effects don’t happen. It means that effects don’t happen as a side effect of mere expression evaluation.
  - Twisol 5y ago
    > Purity doesn’t mean that effects don’t happen. It means that effects don’t happen as a side effect of mere expression evaluation. I don't disagree? I was adding color to your explanation for other readers, not attempting to correct you. The evaluation of a program merely reduces or simplifies it, transforming its structure without adding or removing information. When we can't reduce further without interacting with the environment, something else must mediate that interaction. > That would be equally true of a programming model where every program is a pure function from a list of input lines to a list of output lines. Indeed, Haskell used this model (`[Request] -> [Response]`) before switching to use an IO monad. It made for a poor architectural basis for complex programs.
- goto11 5y ago
  But isn't it the case in any programming language that impure operations only have side effects when they are executed? You might as well argue that a JavaScript program on its own is pure - it is only when it is executed by the runtime it has side effects. You can also pass a function around without executing it in JavaScript.
  - pwm 5y ago
    A good mental model is that Haskell has expressions that are evaluated and JavaScript has statements that are executed. const io_actions = ["hello", "world"].map(s => console.log(s)); io_actions[1]; vs. io_actions = map putStrLn ["hello", "world"] main = io_actions !! 1 JS will print out "hello" and "world" and the value of io_actions[0] is undefined. In Haskell, the value of io_actions !! 0 is IO "world" which is just a value you can pass around in your program. Only when the Haskell runtime evaluates your code is when it will do the effect, which is to print "world". "hello" is never printed. Naturally you can also pattern match on IO (): f :: IO () f = case putStrLn "hello" of _ -> putStrLn "world" also only prints "world". The IO type in Haskell is akin to IO (State World -> (State World, a)), ie. the state monad where the state threaded through the computation is the "real world". This can be demonstrated with the following: f :: IO () f = IO $ \world -> case putStrLn "foo" of IO _ -> case putStrLn "bar" of IO g -> g world prints "bar".
    - goto11 5y ago
      The JavaScript equivalent would be: const io_actions = ["hello", "world"].map(s => () => console.log(s)); io_actions[1](); which also prints "world" when the JavaScript runtime evaluates the code.
      - pwm 5y ago
        If your point is that one can implement a Haskell like language in any turing complete programming language then sure, you are correct. GP's point however was that Haskell is purposefully designed to be written and thought about this way from the ground up. Ie. putStrLn "hello" is not a command that is executed verbatim when the runtime gets to its source position. It's an IO action and an IO action is just a value that can be passed around or, by virtue of IO being a Functor, mapped over, etc... If you say that purity and referential transparency are not only reserved for Haskell then again technically sure, but the point of Haskell is that it makes these concepts the centre of its design. Instead of having to jump through hoops to write code where you can do the above you have to jump through hoops to do the opposite.
Blikkentrekker 5y ago
Your code is not an implementation, only a type theoretical description. 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 coö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.
- 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 ago
    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̄.
goto11 5y ago
This is beside the point. Haskell have a number of built-in unpure operations like putStrLn. You can use the built-in IO type to execute these unpure operations. If you define your own type called IO you can't use it to execute unpure operations.

Twisol 5y ago

You're right, but I think there's a distinction here that is easy to miss. An IO action describes what to do, but something still has to do that action. A Haskell program on its own doesn't do anything; that's exactly why it's pure. The Haskell runtime interprets an IO value, unraveling it into the string of commands that comprise it. The runtime executes the commands produced by the Haskell program. Haskell uses monads exactly because it lets you describe/express complex sequences of actions (for which later actions depend on earlier actions) without requiring that the machinery for actually performing those actions be part of the program too.

anderskaseorg 5y ago
That would be equally true of a programming model where every program is a pure function from a list of input lines to a list of output lines. Everyone would agree that such a model is pure (if limiting), even though the function itself is just a function, and the language runtime takes care of the ugly low-level details of actually making the system calls that read lines from STDIN and write lines to STDOUT. Purity doesn’t mean that effects don’t happen. It means that effects don’t happen as a side effect of mere expression evaluation.
- Twisol 5y ago
  > Purity doesn’t mean that effects don’t happen. It means that effects don’t happen as a side effect of mere expression evaluation. I don't disagree? I was adding color to your explanation for other readers, not attempting to correct you. The evaluation of a program merely reduces or simplifies it, transforming its structure without adding or removing information. When we can't reduce further without interacting with the environment, something else must mediate that interaction. > That would be equally true of a programming model where every program is a pure function from a list of input lines to a list of output lines. Indeed, Haskell used this model (`[Request] -> [Response]`) before switching to use an IO monad. It made for a poor architectural basis for complex programs.
goto11 5y ago
But isn't it the case in any programming language that impure operations only have side effects when they are executed? You might as well argue that a JavaScript program on its own is pure - it is only when it is executed by the runtime it has side effects. You can also pass a function around without executing it in JavaScript.
- pwm 5y ago
  A good mental model is that Haskell has expressions that are evaluated and JavaScript has statements that are executed. const io_actions = ["hello", "world"].map(s => console.log(s)); io_actions[1]; vs. io_actions = map putStrLn ["hello", "world"] main = io_actions !! 1 JS will print out "hello" and "world" and the value of io_actions[0] is undefined. In Haskell, the value of io_actions !! 0 is IO "world" which is just a value you can pass around in your program. Only when the Haskell runtime evaluates your code is when it will do the effect, which is to print "world". "hello" is never printed. Naturally you can also pattern match on IO (): f :: IO () f = case putStrLn "hello" of _ -> putStrLn "world" also only prints "world". The IO type in Haskell is akin to IO (State World -> (State World, a)), ie. the state monad where the state threaded through the computation is the "real world". This can be demonstrated with the following: f :: IO () f = IO $ \world -> case putStrLn "foo" of IO _ -> case putStrLn "bar" of IO g -> g world prints "bar".
  - goto11 5y ago
    The JavaScript equivalent would be: const io_actions = ["hello", "world"].map(s => () => console.log(s)); io_actions[1](); which also prints "world" when the JavaScript runtime evaluates the code.
    - pwm 5y ago
      If your point is that one can implement a Haskell like language in any turing complete programming language then sure, you are correct. GP's point however was that Haskell is purposefully designed to be written and thought about this way from the ground up. Ie. putStrLn "hello" is not a command that is executed verbatim when the runtime gets to its source position. It's an IO action and an IO action is just a value that can be passed around or, by virtue of IO being a Functor, mapped over, etc... If you say that purity and referential transparency are not only reserved for Haskell then again technically sure, but the point of Haskell is that it makes these concepts the centre of its design. Instead of having to jump through hoops to write code where you can do the above you have to jump through hoops to do the opposite.

Blikkentrekker 5y ago

Your code is not an implementation, only a type theoretical description. 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 coö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.

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 ago
  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̄.

goto11 5y ago

This is beside the point. Haskell have a number of built-in unpure operations like putStrLn. You can use the built-in IO type to execute these unpure operations. If you define your own type called IO you can't use it to execute unpure operations.