[Haskell-cafe] On the purity of Haskell

[Conal Elliott]

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".

  - Conal
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120102/11cff35d/attachment.htm>