HaskellDan Doel · 22 July 2015

On the unsafety of interleaved I/O

One area where I'm at odds with the prevailing winds in Haskell is lazy I/O. It's often said that lazy I/O is evil, scary and confusing, and it breaks things like referential transparency. Having a soft spot for it, and not liking most of the alternatives, I end up on the opposite side when the topic comes up, if I choose to pick the fight. I usually don't feel like I come away from such arguments having done much good at giving lazy I/O its justice. So, I thought perhaps it would be good to spell out my whole position, so that I can give the best defense I can give, and people can continue to ignore it, without costing me as much time in the future. :)

So, what's the argument that lazy I/O, or unsafeInterleaveIO on which it's based, breaks referential transparency? It usually looks something like this:

swap (x, y) = (y, x)

setup = do
  r1 < - newIORef True
  r2 <- newIORef True
  v1 <- unsafeInterleaveIO $ do writeIORef r2 False ; readIORef r1
  v2 <- unsafeInterleaveIO $ do writeIORef r1 False ; readIORef r2
  return (v1, v2)

main = do
  p1 <- setup
  p2 <- setup
  print p1
  print . swap $ p2

I ran this, and got:

(True, False)
(True, False)

So this is supposed to demonstrate that the pure values depend on evaluation order, and we have broken a desirable property of Haskell.

First a digression. Personally I distinguish the terms, "referential transparency," and, "purity," and use them to identify two desirable properties of Haskell. The first I use for the property that allows you to factor your program by introducing (or eliminating) named subexpressions. So, instead of:

f e e

we are free to write:

let x = e in f x x

or some variation. I have no argument for this meaning, other than it's what I thought it meant when I first heard the term used with respect to Haskell, it's a useful property, and it's the best name I can think of for the property. I also (of course) think it's better than some of the other explanations you'll find for what people mean when they say Haskell has referential transparency, since it doesn't mention functions or "values". It's just about equivalence of expressions.

Anyhow, for me, the above example is in no danger of violating referential transparency. There is no factoring operation that will change the meaning of the program. I can even factor out setup (or inline it, since it's already named):

main = let m = setup
  in do p1 < - m
        p2 <- m
        print p1
        print . swap $ p2

This is the way in which IO preserves referential transparency, unlike side effects, in my view (note: the embedded language represented by IO does not have this property, since otherwise p1 could be used in lieu of p2; this is why you shouldn't spend much time writing IO stuff, because it's a bad language embedded in a good one).

The other property, "purity," I pull from Amr Sabry's paper, What is a Purely Functional Language? There he argues that a functional language should be considered "pure" if it is an extension of the lambda calculus in which there are no contexts which observe differences in evaluation order. Effectively, evaluation order must only determine whether or not you get an answer, not change the answer you get.

This is slightly different from my definition of referential transparency earlier, but it's also a useful property to have. Referential transparency tells us that we can freely refactor, and purity tells us that we can change the order things are evaluated, both without changing the meaning of our programs.

Now, it would seem that the original interleaving example violates purity. Depending on the order that the values are evaluated, opponents of lazy I/O say, the values change. However, this argument doesn't impress me, because I think the proper way to think about unsafeInterleaveIO is as concurrency, and in that case, it isn't very strange that the results of running it would be non-deterministic. And in that case, there's not much you can do to prove that the evaluation order is affecting results, and that you aren't simply very unlucky and always observing results that happen to correspond to evaluation order.

In fact, there's something I didn't tell you. I didn't use the unsafeInterleaveIO from base. I wrote my own. It looks like this:

unsafeInterleaveIO :: IO a -> IO a
unsafeInterleaveIO action = do
  iv < - new
  forkIO $
    randomRIO (1,5) >>= threadDelay . (*1000) >>
    action >>= write iv
  return . read $ iv

iv is an IVar (I used ivar-simple). The pertinent operations on them are:

new :: IO (IVar a)
write :: IVar a -> a -> IO ()
read :: IVar a -> a

new creates an empty IVar, and we can write to one only once; trying to write a second time will throw an exception. But this is no problem for me, because I obviously only attempt to write once. read will block until its argument is actually is set, and since that can only happen once, it is considered safe for read to not require IO. [1]

Using this and forkIO, one can easily write something like unsafeInterleaveIO, which accepts an IO a argument and yields an IO a whose result is guaranteed to be the result of running the argument at some time in the future. The only difference is that the real unsafeInterleaveIO schedules things just in time, whereas mine schedules them in a relatively random order (I'll admit I had to try a few times before I got the 'expected' lazy IO answer).

But, we could even take this to be the specification of interleaving. It runs IO actions concurrently, and you will be fine as long as you aren't attempting to depend on the exact scheduling order (or whether things get scheduled at all in some cases).

In fact, thinking of lazy I/O as concurrency turns most spooky examples into threading problems that I would expect most people to consider rather basic. For instance:

Don't pass a handle to another thread and close it in the original.
Don't fork more file-reading threads than you have file descriptors.
Don't fork threads to handle files if you're concerned about the files being closed deterministically.
Don't read from the same handle in multiple threads (unless you don't care about each thread seeing a random subsequence of the stream).

And of course, the original example in this article is just non-determinism introduced by concurrency, but not of a sort that requires fundamentally different explanation than fork. The main pitfall, in my biased opinion, is that the scheduling for interleaving is explained in a way that encourages people to try to guess exactly what it will do. But the presumption of purity (and the reordering GHC actually does based on it) actually means that you cannot assume that much more about the scheduling than you can about my scheduler, at least in general.

This isn't to suggest that lazy I/O is appropriate for every situation. Sometimes the above advice means that it is not appropriate to use concurrency. However, in my opinion, people are over eager to ban lazy I/O even for simple uses where it is the nicest solution, and justify it based on the 'evil' and 'confusing' ascriptions. But, personally, I don't think this is justified, unless one does the same for pretty much all concurrency.

I suppose the only (leading) question left to ask is which should be declared unsafe, fork or ivars, since together they allow you to construct a(n even less deterministic) unsafeInterleaveIO?

[1] Note that there are other implementations of IVar. I'd expect the most popular to be in monad-par by Simon Marlow. That allows one to construct an operation like read, but it is actually less deterministic in my construction, because it seems that it will not block unless perhaps you write and read within a single 'transaction,' so to speak.

In fact, this actually breaks referential transparency in conjunction with forkIO:

deref = runPar . get

randomDelay = randomRIO (1,10) >>= threadDelay . (1000*)

myHandle m = m `catch` \(_ :: SomeExpression) -> putStrLn "Bombed"

mySpawn :: IO a -> IO (IVar a)
mySpawn action = do
  iv < - runParIO new
  forkIO $ randomDelay >> action >>= runParIO . put_ iv
  return iv

main = do
  iv < - mySpawn (return True)
  myHandle . print $ deref iv
  randomDelay
  myHandle . print $ deref iv

Sometimes this will print "Bombed" twice, and sometimes it will print "Bombed" followed by "True". The latter will never happen if we factor out the deref iv however. The blocking behavior is essential to deref maintaining referential transparency, and it seems like monad-par only blocks within a single runPar, not across multiples. Using ivar-simple in this example always results in "True" being printed twice.

It is also actually possible for unsafeInterleaveIO to break referential transparency if it is implemented incorrectly (or if the optimizer mucks with the internals in some bad way). But I haven't seen an example that couldn't be considered a bug in the implementation rather than some fundamental misbehavior. And my reference implementation here (with a suboptimal scheduler) suggests that there is no break that isn't just a bug.

Discussion

Derek ElkinsJuly 22nd, 2015 at 5:04 pm

I will present counterargument to the claims you actually bring up.

First, I completely agree with your definition of referential transparency (and agree that it is widely misused). I also will take your definition of purity for lack of a better one. (It’s the definition I would point to if forced to give one.)

On to counter-argument:

Channelling Lennart, my first retort is “show me the semantics”. It is not enough to say “well IO actions have basically no semantics anyway so anything is allowed”. That’s certainly not true for most IO actions, and saying a particular one has no semantics is hardly a compelling argument for it. Luckily for you, you DID actually show a semantics. Unluckily, I disagree that it reasonably reflects unsafeInterleaveIO. In particular, I imagine most people would expect fmap (const ()) (unsafeInterleaveIO (putStrLn “foo”)) to print nothing ever. “But,” you interject, “GHC is perfectly free to evaluate things speculatively!” I agree. Hell, I’d go further. Even if you use it, GHC would be free to not evaluate it, if, for example, it could prove that it always would return (). Still, it’s possible the threadDelay could never return. The real clincher is GHC is free to evaluate it *multiple* times. That means that in “n <- unsafeInterleaveIO (readIORef r >>= writeIORef r . succ)”, n can be any number greater than whatever r is initialized to. So the real unsafeInterleaveIO is a lot *less* deterministic than your definition. “Still,” you splutter, “I can have my unsafeInterleaveIO simply randomly decide to execute action an arbitrary number of times randomly returning one of the results.” That’s still not enough. Your definition will never lead to n /= n but unsafeInterleaveIO can (just assume call-by-name, or, in GHC, hope for a thunk to be entered twice). Does Sabry’s purity impress you now?

[While it's quite possible that monad-par's IVars are broken, and ivar-simple's semantics are certainly nicer, I think all you are demonstrating with this particular example is the (unpleasant but defined) semantics of asynchronous exceptions. Note, deref or any expression could just as well throw a stack overflow exception the first time but not the second. The semantics for asynchronous exceptions accounts for this.]

Derek ElkinsJuly 23rd, 2015 at 2:19 am

So, I actually wrote up a whole response before providing the one above. I went with the above because it is a more black and white argument (and it directly addresses Sabry’s notion of purity.*)

At any rate, my retort is still “show me the semantics”. If we want to go by the guarantees GHC (strives to) provides, then I would say your definition really is simply wrong.** I await the version that only executes if forced. If you think your definition is still adequate, then we agree: unsafeInterleaveIO is unnecessary. To be clear (and less snarky), your argument that it “isn’t really that unsafe” is by analogy to concurrency, but concurrency in Haskell doesn’t depend on evaluation order where, I say, unsafeInterleaveIO definitionally does.

I will omit (for now) all the software engineering arguments against unsafeInterleaveIO (of the sort that, well-defined or not, it’s a bad idea), except to acknowledge that there are software engineering arguments *for* unsafeInterleaveIO, but I (personally) find them no different in kind and less compelling than the arguments for mutable state or continuations.

For monad-par, because I’m pretty confident runPar and co. do nothing to keep thunks from entering twice, this doesn’t violate referential transparency. I.e. that “the latter” could happen if deref iv was factored out (albeit it’s extremely unlikely, in fact, I believe impossible for this particular example and GHC in reality, but not theoretically impossible or something the GHC implementation would go out of its way to avoid in similar scenarios). I think this side discussion is a red herring though.

* To be clear, Sabry’s paper argues that lazy ST violates his notion of purity. I am willing to support arguments for its modification/removal. I’m not as motivated, though, since people don’t actually seem to be making fragile code depending on it (because they don’t actually seem to be using it at all…)

** I think every implementation of Haskell ever would provide the guarantee. I’m less confident about the eager-but-non-strict speculative evaluation implementations, but I suspect even they too give this guarantee or would strive to, potentially by hacking the definition of unsafeInterleaveIO.

Derek ElkinsJuly 23rd, 2015 at 4:14 am

To avoid ping-ponging, what I’m saying is that your argument and response come off as playing both sides of “evaluation order is (un)defined”. For your definition to be a valid interpretation relies on the very loosely constrained evaluation order of Haskell. I’m more than willing to give you that, but you have to give me every other interpretation that Haskell’s semantics allows. If you don’t, and hold me to GHC’s evaluation order, then, as I did, I will hold your definition, or any other definition you could provide, to GHC’s evaluation order, in which case it definitely is not a valid interpretation or else unsafeInterleaveIO wouldn’t need to be a primitive.

Dan DoelJuly 23rd, 2015 at 6:26 pm

Making GHC schedule things the same way it does for unsafeInterleaveIO isn’t difficult. It but most IVar packages aren’t set up for doing it. Doing it looks like this:

http://lpaste.net/4819527135217582080

It can also be implemented using Ed’s promises package, but it isn’t intended to be used with IO (so forcing IO into the promise monad is unsafe in general), the implementation is much more complicated, and the construction of unsafeInterleaveIO is too simple to be instructive:

unsafeInterleaveIO action = runLazyIO_ $ \p -> unsafePrimToPrim action >>= (!=) p

But of course, all this only fixes the precise scheduling. If you use my random scheduling to implement getContents, for instance, it gives the right answer; it just reads ahead, so it isn’t very good at being lazy.

–

It’s not true that concurrency in (GHC) Haskell doesn’t depend on evaluation order. Threads can’t be interrupted if they’re evaluating things that don’t do any allocation. So, scheduling will be different depending on when exactly certain optimized loops are evaluated.

But to be honest, I don’t really care. “Use an oracle to figure out how to run things at exactly the moment they’re needed elsewhere,” is a fine description of a scheduler, if you can implement it. And in the limited case of unsafeInterleaveIO, GHC can. It’s not the sort of scheduler people are used to using; it’s more like cooperative concurrency. But I don’t expect to be very impressed by any arguments that try to say that scheduling things according to a more cooperative strategy is less ’safe’ than scheduling things randomly.

–

usafeInterleaveST is not at all comparable to unsafeInterleaveIO. This is because ST has as part of its specification a safe operation:

runST :: (forall s. ST s a) -> a

You cannot safely add any non-determinism to ST because of this. fork and random number generation (without being based deterministically on some passed-in seed) are also not allowable.

–

runPar uses unsafePerformIO, which also prevents IO actions from being executed twice via duplicate thunk entering in GHC. Presumably this is because it is now used for situations where it would be undesirable for the duplication to occur, unlike the original intentions of the FFI (where you’d probably only be reading pointers that would never change).

Talking about monad-par is probably not important. But the no-duplication property is important for unsafeInterleaveIO, at least. It would be inadequate for implementing the things it’s intended to implement if it didn’t ensure it, or if there weren’t something else that ensured it. But it might as well be rolled into unsafeInterleaveIO itself (and since as far as I can tell, there’s no actual specification of unsafeInterleaveIO outside of base, I don’t feel very bad taking it to be part of the operation).

Dan DoelJuly 24th, 2015 at 12:40 am

If we’re going to stipulate that concurrency (in IO) that schedules things in the way that matches GHC’s unsafeInterleaveIO is impure, then I don’t think I believe that any scheduler that anyone would actually implement is pure, either. In fact, I don’t think the one that GHC uses would count as pure, even if non-allocating code could be preempted. And I think many other “safe” IO features would count as impure, as well. IO would have to be largely thrown out, so at that point it isn’t even worth discussing whether unsafeInterleaveIO as implemented conserves purity.

Also, I don’t think I ever implied that GHC’s thread scheduler was specified to be the oracle scheduler. My point was that the way unsafeInterleaveIO behaves would be like having a second concurrency system that did schedule things that way, and included fork and IVar.

And finally, and maybe I didn’t get this across well enough, I think it’s not exactly worth caring whether what exactly happens is pure if you work out the details (and, I think I agree with your * there). _Define_ unsafeInterleaveIO to be pure, and rather arbitrarily interleaving, because you do not know the exact order that GHC will evaluate your code in, without looking at the output of the compiler. Even most of the tools people like to believe enforce ordering do not.

In practice the scheduling will match some selected evaluation order, but you cannot (necessarily) easily know that order. But quotienting by concerns like that is like purity, and is rather the point of purity (you don’t need to worry about the things you can’t know).

Derek ElkinsJuly 24th, 2015 at 7:03 pm

My point is that the semantics of concurrency are non-deterministic and so, at the level of semantics, you get a set of possible meanings. This set doesn’t change when you change evaluation order. It may well be that the particular *implementation* guarantees a specific meaning or a smaller subset of meanings, and further, that changing the evaluation order would lead to a different subset of meanings, but since I’m ignorant of that implementation detail, to me the meaning is the larger set, and that set is invariant with respect to evaluation order modulo termination.

I would say most schedulers including GHC’s (modulo things that would be considered bugs) provide evaluation order invariant semantics. (To be clear: evaluation is NOT execution of the IO monad.) If I switch Haskell from a call-by-need language to a call-by-value, modulo some programs not terminating anymore, I’m pretty confident that the results I see from concurrent programs will be just the same. At worst, they may differ, but only in ways that I would have accepted as correct before (- they just happened not to happen before).

I’m perfectly fine with unsafeInterleaveIO existing.* We can say that the semantics is similar to your original post. If I write a program that works correctly given that semantics, but just happens to be a lot more efficient if unsafeInterleaveIO just happens to follow evaluation order, then *wink* *wink*, *nod* *nod*, unsafeInterleaveIO may be a good choice.

Unfortunately, people don’t do this. They write programs *relying* on unsafeInterleaveIO having a specific semantics related to evaluation order, and when things go wrong, they enter the losing game of trying to control evaluation order. With your ivar-simple-based definition, evaluation order is irrelevant; trying to control it is a non sequitur.

If you still don’t understand what I’m saying (and think I’m saying something different from what I am saying), this is my last attempt: If we change the evaluation order of Haskell to call-by-value, then, modulo being strict (note: strict NOT eager), your definition of unsafeInterleaveIO in terms of ivar-simple will mean *exactly* the same thing. The specification of unsafeInterleaveIO in terms of evaluation order would *obviously* change. In fact, that specification would make unsafeInterleaveIO = id in the case of call-by-value which it observably is not in the case of call-by-need (as demonstrated by fmap (const ())). My argument the whole time is the difference between what your program MEANS versus what it DOES. Evaluation order is highly relevant to what it DOES, but should not change what it MEANS (modulo termination). Modulo termination, nothing in Safe Haskell can change the MEANING of your program if the evaluation order changes (i.e. nothing can observe evaluation order in a usable way). unsafeInterleaveIO breaks this property UNLESS you define it to have a broad semantics. If you do, that makes a program using it also have a broad semantics. If you want your program to have a definite meaning, you will need to tolerate unsafeInterleaveIO’s broad semantics. Once you’ve gotten the desired meaning for your program you can THEN use what unsafeInterleaveIO actually DOES to improve what your program actually DOES which won’t change the MEANING.

* I’m am NOT fine with it being in Prelude functions like readFile though. Not that its “incorrect” to have it there, just that it’s insane. Imagine the semantics *were* the ones from your post. Then readFile is an insane function that I can’t imagine anyone wanting.

Dan DoelJuly 24th, 2015 at 10:32 pm

Well, to be honest, I have no idea what most IO stuff “means,” other than being an (opaque) embedded description telling something else what to do. So it is almost trivial to me that they wouldn’t mean anything different on changing evaluation order, because they barely mean anything to begin with. So when you say that my oracle scheduler is impure, it doesn’t make any sense to me, because the scheduler is part of the ‘doing’ not the ‘meaning.’ And that goes for a lot of other stuff we’ve been talking about. For instance, I don’t think I would say my pasted code means something different than the code from this article. It just does something different.

So I guess we’re on the same page? I think if you want to talk about meaning, you can’t tell much about unsafeInterleaveIO. Even if you want to talk about doing, you can’t necessarily tell much. For instance, for the program I began with, people expect to see:

(True, False)
(True, False)

printed on their screen. But nothing actually says they won’t see any of the other output my random delay version produces. Because there is no guarantee that GHC will evaluate the tuple components left-to-right, and there’s no guarantee that it will choose the same evaluation order both times. And all that is true no matter how many seqs you bury the code in. So, inasmuch as unsafeInterleaveIO _does_ something that corresponds to a valid Haskell evaluation order, what it does is completely non-deterministic in this example. GHC isn’t actually crazy enough to make it output all the different possibilities (in this case, at least). But there’s nothing that says you can rely on that.

Derek ElkinsJuly 25th, 2015 at 9:38 pm

The IOSpec library gives a very concrete answer to the semantics of many features of IO. To model concurrency, you just add a CPS aspect to the model of IO, implement a cooperative scheduler, and throw a yield into the denotation of (>>=). Now, that will be deterministic, but all you need to do then is define the scheduler as a non-deterministic choice between the runnable threads. This already is enough for most purposes, e.g. this is adequate to give the (True,False), (False,True), and (False,False) answers in your example. You can even handle the relaxed consistency memory model for IORefs by adding an explicit notion of “thread”, having writeIORef add to a “pending writes” set state component (in addition to updating a thread-local heap as normal), and readIORef non-deterministically chooses to commit zero or more pending writes (from other threads) to the thread-local heap before reading. Possibly, the most awkward part is dealing with non-termination at the value level (i.e. fix id). It’s possible just using an angelic non-deterministic operator will handle this. At any rate, it’s solvable, it’s just a matter of doing it in a clean, modular way that’s not necessarily completely obvious.

I/O is actually pretty easy. The problem isn’t that I/O operations in the IO monad don’t have semantics but that the “OS” doesn’t have semantics. The semantics from the IO monad’s perspective is a request/response denotation similar to the meaning of conduit or pipes. Given no semantics for the “OS”, you are correct that the meaning of hGetChar is that, if the response is ever received, it can be any character or an error result (or an, unrelated, asynchronous exception). But that doesn’t stop IO from being *completely* specified.

Still, as before, you do actually believe the “OS” operations have some semantics or else you would have no reason to call any of them. So you can imagine and make models of “OS” that refine the completely free semantics above. IOSpec has an example of this. Whether your model is actually sound with respect to the actual OS is a different question.

If it wasn’t clear before, I do believe that your oracle scheduler is a completely legitimate (but not complete) refinement of the scheduler I sketched above. I never intended to imply that such a scheduler was disallowed if you got that impression. The difference is, to refine the scheduler to, say, a round-robin scheduler, requires knowing and changing nothing about how expressions are evaluated*. To have your oracle scheduler requires invasive changes to the meaning of evaluation. This is what I meant about it being impure. I think you’ll agree that there are many schedulers, including most textbook ones, that can be written without such a change. (There are also many for which it’s not obvious that you can. For example, if I want to schedule based on which thread is using the most memory, then I need to know how much memory evaluation uses.)

To conclude, the *only* reason I view unsafeInterleaveIO as unsafe is *because* it makes evaluation order observable. If it had semantics similar to your definition, I obviously couldn’t complain since it’s a readily definable safe function. The appellation “unsafe” would be unwarranted. It would then just be sillyInterleaveIO**, and I think few people would ever want to use it, and they certainly couldn’t be surprised by the behavior it gives, and they certainly wouldn’t try to solve the races it can give rise to by throwing seqs around.

* To be a bit more precise, we have a denotation function that turns expressions into values (evaluation), and then a separate denotation function that gives IO values semantics (execution). The second uses the first, but the first doesn’t use the second and needn’t know anything about the second. This is why the IO monad doesn’t make Haskell impure. To handle your oracle scheduler or unsafeInterleaveIO directly requires that the first denotation function must cooperate with the second. For example, by returning, in addition to the value, a data structure describing the complete reduction order.

** A better name might be “race”.

Dan DoelJuly 25th, 2015 at 11:14 pm

I think most people want to use schedulers that provide some kind of fairness guarantees. And they expect that fairness to be based on how much time the thread has run, including evaluation. So, I mean what I said before: I think most schedulers that people would actually use are impure if you’re going to take the scheduler into account as part of the ‘meaning’.

Same with I/O stuff. The OS has things happening concurrently entirely out of your program’s control, and it isn’t waiting for you to yield so that scheduling can be ‘pure’. With other programs modifying files, evaluation order is going to affect what you see those files containing. And it doesn’t even help if you imagine that you have as many parallel processors as you have processes (so that you don’t really need to schedule anything per se), because evaluation order will still affect the relative ordering of accesses to shared state.

And of course, anything that lets you access the current time is probably impure.

You could just say that that’s not part of the ‘meaing,’ or that you’re not going to model it. But then I don’t see why I can’t say that unsafeInterleaveIO is specified to be nondeterministic, but in practice something good happens that we’re not going to model.

And I might still use sillyInterleaveIO. I probably wouldn’t use it to read and write to IORefs; but I wouldn’t do that anyway. sillyReadFile is still just a better version of strictReadFile for many uses, because it lets work get done concurrently with the file being read in (and memory getting eaten). And it retains the nice interface of strictReadFile, instead of having an interface I dislike. The big problem is that the IVars add even more overhead. :)

Derek ElkinsJuly 26th, 2015 at 6:46 am

For them to be impure, they’d need some way of connecting evaluation to time. A pure specification doesn’t preclude an impure realization. Most schedulers don’t schedule a number of reductions but a number of milliseconds. You’re going from some expression evaluating in an unknown number of milliseconds under one evaluation order to a possibly different unknown number of milliseconds in another. Either way it’s an unknown. A model can’t distinguish between these unless you model the time evaluation takes, and no one is proposing specifying that. Similarly for OS calls. To put it another way, given a complete model (complete in the model theory sense which implies that anything you can prove it in is true for every other sound model, i.e. it’s a model that makes no assumptions), how would you go about showing that changing the evaluation order (say the model is parameterized by an “evaluation order” function) would lead to different results? A model where reductions take zero time or a model where reductions take 10 billion years are both valid refinements of the complete model. If the Haskell Report said, “beta reductions take 30ns”, then Haskell would not be a pure language because different evaluation orders would lead to denotations that differed in more than just whether they terminated or not.

You *can* say unsafeInterleaveIO is specified to be nondeterministic. That’s what I *have* been recommending. However, you can’t specify it as following evaluation order without modeling and depending on evaluation order. It’s completely fine for the specification to be non-deterministic and the implementation to follow evaluation order. But to make claims about the meaning/correctness of your program you have to do it against the specification, not the implementation details. It’s clear that, at least in people’s minds, unsafeInterleaveIO is specified as following evaluation order (and that evaluation order is constrained to something reasonable). Believing that unsafeInterleaveIO executes the action at some non-deterministic point in the future gives absolutely no license or reason to believe that adding seq somewhere will reliably change anything. By such a definition, a program using unsafeInterleaveIO that does something incorrect cannot be fixed by adding seq.

We may completely agree extensionally if not intensionally, at least about unsafeInterleaveIO. As a check, would you agree with the following statements:
1) For a person to claim their code using unsafeInterleaveIO is correct, it must also be correct with regards to implementations like the one you gave.
2) Adding things like seq and such cannot make incorrect code correct, though it may make incorrect code work for a particular implementation.

Dan DoelJuly 26th, 2015 at 6:42 pm

Yes, I think I would agree with those statements. Although I’m tempted to write incorrect code that works at times. For instance, when people complain about running out of file descriptors with `mapM` readFile l, one way to make it work is to interleave the mapM. But that is not correct, since it may (or may not) start too many threads and still use up all file descriptors (although, if you have to handle more than 1,000 files, maybe you shouldn’t use lazy I/O, much as it pains me to say).

–

To quibble some more, it’s not clear to me how IVar isn’t in violation of your specification, either. Sometimes evaluation has to stop to block on the value of a concurrent reference cell. So it seems to me, prima facie, that evaluation is going to have to be modified to work together with execution. You need yield points not just as part of IO execution, but evaluation as well.

There will exist terms for which different evaluation orders yield differently. In the barest way of modeling this that I can think of, there will be a different number of yields. However, if you want to model what any good implementation would probably do, evaluation would yield with a specification of which IVar needs to be written to, so that we don’t need to bother trying to resume evaluation on something that will immediately re-yield.

But this is exactly the information a scheduler needs to implement unsafeInterleaveIO as GHC does. It’s why I was able to do it so easily in my paste. value already calls out to IO, there’s just no ‘wait until this MVar needs to be filled’ primitive, so I added a second MVar directly.

I guess monad-par makes one answer clear: you don’t know that ‘value’ won’t just throw an exception. In monad-par it does if the IVar hasn’t been written yet. So that’s the pure semantics; you may or may not get a value. And the implementation of ivar-simple blocks and tries to get you an answer if one can be gotten.

Yet, people are pretty okay with IVars, and not unsafeInterleaveIO, even though they look pretty similar to me, any way you want to slice it.

Download Markdown