[Haskell-cafe] On the purity of Haskell
conal at conal.net
Mon Jan 2 19:30:35 CET 2012
On 2012/1/1 Ertugrul Söylemez <es at ertes.de> wrote:
> Steve Horne <sh006d3592 at 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".
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe