Re: [Haskell-cafe] On the purity of Haskell

On 2012/1/1 Ertugrul Söylemez wrote:

Steve Horne wrote:

...

Of course even the bind operator arguably isn't primitive. We could translate to get rid of those too, and see what lies underneath. This is where we start seeing functions of type...

World -> (x, World)

Problem - this level of abstraction is hypothetical. It is not part of the Haskell language. Haskell specifically defines the IO monad to be a black box.

And that's fine, because IO is an embedded DSL. A better view of IO is a GADT like:

data IO :: * -> * where GetLine :: IO String PutStrLn :: String -> IO () ...

This is still hypothetical, but it shows how even IO is easily referentially transparent (as long as you don't use unsafe* cheats).

What?? I see how a definition like this one shows how something else that you call "IO" can be denotative & RT. I don't see how what that conclusion has to do with Haskell's IO. I also wonder whether you're assuming that all of the IO primitives we have in Haskell treat their non-IO arguments denotationally/extensionally, so that there cannot be operations like "isWHNF :: a -> IO Bool". - Conal