Steve Horne <sh006d3592@blueyonder.co.uk> 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