On 2012/1/1 Ertugrul Söylemez <span dir="ltr"><<a href="mailto:es@ertes.de">es@ertes.de</a>></span> wrote:<br><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class="im">Steve Horne <<a href="mailto:sh006d3592@blueyonder.co.uk">sh006d3592@blueyonder.co.uk</a>> wrote:<br>
> Of course even the bind operator arguably isn't primitive. We could<br>
> translate to get rid of those too, and see what lies underneath. This<br>
> is where we start seeing functions of type...<br>
><br>
> World -> (x, World)<br>
><br>
> Problem - this level of abstraction is hypothetical. It is not part of<br>
> the Haskell language. Haskell specifically defines the IO monad to be<br>
> a black box.<br>
<br>
</div>And that's fine, because IO is an embedded DSL. A better view of IO is<br>
a GADT like:<br>
<br>
data IO :: * -> * where<br>
GetLine :: IO String<br>
PutStrLn :: String -> IO ()<br>
...<br>
<br>
This is still hypothetical, but it shows how even IO is easily<br>
referentially transparent (as long as you don't use unsafe* cheats).<br></blockquote><div><br>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.<br>
<br>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".<br>
<br> - Conal<br></div></div>