Unsafe hGetContents

[Heinrich Apfelmus]

Iavor Diatchki wrote:
> Hello,
> 
> well, I think that the fact that we seem to have a program context
> that can distinguish "f1" from "f2" is worth discussing because I
> would have thought that in a pure language they are interchangable.
> The question is, does the context in Oleg's example really distinguish
> between "f1" and "f2"?  You seem to be saying that this is not the
> case:  in both cases you end up with the same non-deterministic
> program that reads two numbers from the standard input and subtracts
> them but you can't assume anything about the order in which the
> numbers are extracted from the input---it is merely an artifact of the
> GHC implementation that with "f1" the subtraction always happens the
> one way, and with "f2" it happens the other way.
>
> I can (sort of) buy this argument, after all, it is quite similar to
> what happens with asynchronous exceptions (f1 (error "1") (error "2")
> vs f2 (error "1") (error "2")).  Still, the whole thing does not
> "smell right":  there is some impurity going on here, and trying to
> offload the problem onto the IO monad only makes reasoning about IO
> computations even harder (and it is petty hard to start with).  So,
> discussion and alternative solutions should be strongly encouraged, I
> think.

To put it in different words, here an elaboration on what exactly the
non-determinism argument is:


Consider programs  foo1  and  foo2  defined as

    foo :: (a -> b -> c) -> IO String
    foo f = Control.Exception.catch
            (evaluate (f (error "1") (error "2")) >> return "3")
            (\(ErrorCall s) -> return s)

    foo1  = foo f1  where  f1 x y = x `seq` y `seq` ()
    foo2  = foo f2  where  f2 x y = y `seq` x `seq` ()

Knowing how exceptions and  seq  behave in GHC, it is straightforward to
prove that

    foo1  = return "1"
    foo2  = return "2"

which clearly violates referential transparency. This is bad, so the
idea is to disallow the proof.


In particular, the idea is that referential transparency can be restored
if we only allow proofs that work for all evaluation orders, which is
equivalent to introducing non-determinism. In other words, we are only
allowed to prove

    foo1  = return "1"  or  return "2"
    foo2  = return "1"  or  return "2"

Moreover, we can push the non-determinism into the IO type and pretend
that pure functions  A -> B  are semantically lifted to  Nondet A ->
Nondet B  with some kind of  fmap .


The same goes for  hGetContents : if you use it twice on the same
handle, you're only allowed to prove non-deterministic behavior, which
is not very useful if you want a deterministic program. But you are
allowed to prove deterministic results if you use it with appropriate
caution.


In other words, the language semantics guarantees less than GHC actually
does. In particular, the semantics only allows reasoning that is
independent of the evaluation order and this means to treat IO as
non-deterministic in certain cases.


Regards,
apfelmus

--
http://apfelmus.nfshost.com