Am Sonntag, 15. März 2009 21:25 schrieb Jonathan Cast:

On Sun, 2009-03-15 at 13:02 -0700, Ryan Ingram wrote:

...

Furthermore, due to the monad laws, if f is total, then reordering the (x <- ...) and (y <- ...) parts of the program should have no effect. But if you switch them, the program will *always* print 0.

I'm confused. I though if f was strict, then my program *always* printed 1?

But not if you switch the (x <- ...) and (y <- ...) parts: main = do r <- newIORef 0 v <- unsafeInterleaveIO $ do writeIORef r 1 return 1 y <- readIORef r x <- case f v of 0 -> return 0 n -> return (n - 1) print y Now the IORef is read before the case has a chance to trigger the writing.

Am Sonntag, 15. März 2009 21:56 schrieb Jonathan Cast:

On Sun, 2009-03-15 at 21:43 +0100, Daniel Fischer wrote:

...

Am Sonntag, 15. März 2009 21:25 schrieb Jonathan Cast:

...

On Sun, 2009-03-15 at 13:02 -0700, Ryan Ingram wrote:

...

Furthermore, due to the monad laws, if f is total, then reordering the (x <- ...) and (y <- ...) parts of the program should have no effect. But if you switch them, the program will *always* print 0.

I'm confused. I though if f was strict, then my program *always* printed 1?

But not if you switch the (x <- ...) and (y <- ...) parts:

main = do r <- newIORef 0 v <- unsafeInterleaveIO $ do writeIORef r 1 return 1 y <- readIORef r x <- case f v of 0 -> return 0 n -> return (n - 1) print y

Now the IORef is read before the case has a chance to trigger the writing.

But if the compiler is free to do this itself, what guarantee do I have that it won't?

None? Wasn't that Ryan's point, that without the unsafeInterleaveIO, that reordering wouldn't matter, but with it, it does?

jcc

Am Sonntag, 15. März 2009 22:20 schrieb Jonathan Cast:

There is *no* guarantee that main0 prints 0, while main1 prints 1, as claimed. The compiler is in fact free to produce either output given either program, at its option. Since the two programs do in fact have exactly the same set of possible implementations, they *are* equivalent. So the ordering in fact *doesn't* matter.

Hum. Whether the programme prints 0 or 1 depends on whether "writeIORef r 1" is done before "readIORef r". That depends of course on the semantics of IO and unsafeInterleaveIO. In so far as the compiler is free to choose there, it can indeed produce either result with either programme. But I think "Haskell 's I/O monad provides the user with a way to specify the sequential chaining of actions, and an implementation is obliged to preserve this order." (report, section 7) restricts the freedom considerably. However, I understand "unsafeInterleaveIO allows IO computation to be deferred lazily. When passed a value of type IO a, the IO will only be performed when the value of the a is demanded." as explicitly allowing the programmer to say "do it if and when the result is needed, not before". So I think main0 *must* print 0, because the ordering of the statements puts the reading of the IORef before the result of the unsafeInterleaveIOed action may be needed, so an implementation is obliged to read it before writing to it. In main1 however, v may be needed to decide what action's result x is bound to, before the reading of the IORef in the written order, so if f is strict, the unsafeInterleaveIOed action must be performed before the IORef is read and the programme must print 1, but if f is lazy, v is not needed for that decision, so by the documentation, the unsafeInterleaveIOed action will not be performed, and the programme prints 0.

jcc

Am Sonntag, 15. März 2009 23:30 schrieb Jonathan Cast:

On Sun, 2009-03-15 at 23:18 +0100, Daniel Fischer wrote:

...

Am Sonntag, 15. März 2009 22:20 schrieb Jonathan Cast:

...

There is *no* guarantee that main0 prints 0, while main1 prints 1, as claimed. The compiler is in fact free to produce either output given either program, at its option. Since the two programs do in fact have exactly the same set of possible implementations, they *are* equivalent. So the ordering in fact *doesn't* matter.

Hum. Whether the programme prints 0 or 1 depends on whether "writeIORef r 1" is done before "readIORef r". That depends of course on the semantics of IO and unsafeInterleaveIO.

In so far as the compiler is free to choose there, it can indeed produce either result with either programme. But I think "Haskell 's I/O monad provides the user with a way to specify the sequential chaining of actions, and an implementation is obliged to preserve this order." (report, section 7) restricts the freedom considerably.

Why not read that line as prohibiting concurrency (forkIO) as well?

Good question. Because forkIO is a way to explicitly say one doesn't want the one thing necessarily done before the other, I'd say.

...

However, I understand "unsafeInterleaveIO allows IO computation to be deferred lazily. When passed a value of type IO a, the IO will only be performed when the value of the a is demanded."

Where is this taken from? If GHC's library docs try to imply that the

From the documentation of System.IO.Unsafe.

programmer can predict when an unsafeInterleaveIO'd operation takes place --- well, then they shouldn't. I'm starting to suspect that not starting from a proper denotational theory of IO was a major mistake for GHC's IO system (which Haskell 1.3 in part adopted).

Maybe.

...

as explicitly allowing the programmer to say "do it if and when the result is needed, not before".

Haskell's order of evaluation is undefined, so this doesn't really allow the programmer to constrain when the effects are performed much.

The full paragraph from the report: " The I/O monad used by Haskell mediates between the values natural to a functional language and the actions that characterize I/O operations and imperative programming in general. The order of evaluation of expressions in Haskell is constrained only by data dependencies; an implementation has a great deal of freedom in choosing this order. Actions, however, must be ordered in a well-defined manner for program execution -- and I/O in particular -- to be meaningful. Haskell 's I/O monad provides the user with a way to specify the sequential chaining of actions, and an implementation is obliged to preserve this order." I read it as saying that IO *does* allow the programmer to control when the effects are performed.

...

So I think main0 *must* print 0, because the ordering of the statements puts the reading of the IORef before the result of the unsafeInterleaveIOed action may be needed, so an implementation is obliged to read it before writing to it.

In main1 however, v may be needed to decide what action's result x is bound to, before the reading of the IORef in the written order, so if f is strict, the unsafeInterleaveIOed action must be performed before the IORef is read and the programme must print 1,

Although as Ryan pointed out, the compiler may decide to omit the case statement entirely, if it can statically prove that f v is undefined.

I suppose that's a typo and should be "unneeded". But can it prove that f v is unneeded? After all, it may influence whether 0 or 1 is printed.

...

but if f is lazy, v is not needed for that decision, so by the documentation, the unsafeInterleaveIOed action will not be performed, and the programme prints 0.

jcc

Am Montag, 16. März 2009 00:47 schrieb Jonathan Cast:

On Mon, 2009-03-16 at 00:14 +0100, Daniel Fischer wrote:

...

...

...

However, I understand "unsafeInterleaveIO allows IO computation to be deferred lazily. When passed a value of type IO a, the IO will only be performed when the value of the a is demanded."

Where is this taken from? If GHC's library docs try to imply that the

From the documentation of System.IO.Unsafe.

This version of those docs:

http://haskell.org/ghc/docs/latest/html/libraries/base/System-IO-Unsafe.htm l

leaves unsafeInterleaveIO completely un-documented. So I'm still not sure what you're quoting from.

The documentation haddock-0.9 built when I compiled ghc-6.8.3 last year.

...

...

programmer can predict when an unsafeInterleaveIO'd operation takes place --- well, then they shouldn't. I'm starting to suspect that not starting from a proper denotational theory of IO was a major mistake for GHC's IO system (which Haskell 1.3 in part adopted).

Maybe.

...

...

as explicitly allowing the programmer to say "do it if and when the result is needed, not before".

Haskell's order of evaluation is undefined, so this doesn't really allow the programmer to constrain when the effects are performed much.

The full paragraph from the report:

" The I/O monad used by Haskell mediates between the values natural to a functional language and the actions that characterize I/O operations and imperative programming in general. The order of evaluation of expressions in Haskell is constrained only by data dependencies; an implementation has a great deal of freedom in choosing this order. Actions, however, must be ordered in a well-defined manner for program execution -- and I/O in particular -- to be meaningful. Haskell 's I/O monad provides the user with a way to specify the sequential chaining of actions, and an implementation is obliged to preserve this order."

I read it as saying that IO *does* allow the programmer to control when the effects are performed.

Right. But by using forkIO or unsafeInterleaveIO you waive that ability.

That depends on the specification of unsafeInterleaveIO. If it is "unspecified order of evaluation", then yes, if it is "do when needed, not before", as my local documentation can be interpreted, then unsafeInterleaveIO reduces that ability, but doesn't completely remove it.

On Sun, Mar 15, 2009 at 1:56 PM, Jonathan Cast wrote:

...

But not if you switch the (x <- ...) and (y <- ...) parts:

main = do     r <- newIORef 0     v <- unsafeInterleaveIO $ do         writeIORef r 1         return 1     y <- readIORef r     x <- case f v of             0 -> return 0             n -> return (n - 1)     print y

Now the IORef is read before the case has a chance to trigger the writing.

But if the compiler is free to do this itself, what guarantee do I have that it won't?

You don't really have any guarantee; the compiler is free to assume that v is a pure integer and that f is a pure function from integers to integers. Therefore, it can assume that the only observable affect of calling f v is non-termination. Note that unsafeInterleaveIO *breaks* this assumption; that is why it is unsafe. I erred previously in saying that this was allowed if f is total; it does still evaluate f v either way. But I can correct my argument as follows: the only observable effect from the (x <- ...) line is non-termination. And the compiler can prove that there *no* observable effect of "readIORef" until the value is used or the reference is written by another function. So it is free to make this reordering anyways, as the only observable effect could have been non-termination which will be observed immediately after. When you use unsafeInterleaveIO or unsafePerformIO, you are required prove that its use does not break these invariants; that, for example, you don't read or write from IORefs that could be accessed elsewhere in the program. These are proofs that the compiler can and does make in some situations; it can reorder sequential readIORef calls if it thinks one or the other might be more efficient. It can evaluate foldl as if it was foldl' if it proves the arguments strict enough that non-termination behavior is identical (ghc -O2 does this, for example). The language has them as "escape hatches" that allow you to write code that would not otherwise be possible, by shifting more of a proof obligation on to the programmer. -- ryan

...

main = do r <- newIORef 0 v <- unsafeInterleaveIO $ do writeIORef r 1 return 1 x <- case f v of 0 -> return 0 n -> return (n - 1) y <- readIORef r print y

-- a couple of examples: f x = 0 -- program prints "0" -- f x = x -- program prints "1"

"f" is pure. But if f is nonstrict, this program prints 0, and if it's strict, it prints 1. The strictness of a pure function can change the observable behavior of your program!

Strictness is an effect, even if it isn't recorded in Haskell's types. Replacing 'v <- ..' by 'let v = undefined' provides similar choices. 'unsafeInterleaveIO' explicitly uses the "implicit" effects of strictness to drive the "explicit" effects of IO, which is why it is unsafe (moving IO effects from explicit to implicit). But even if 'unsafeInterleaveIO' where eliminated, strictness/evaluation would still remain as an implicit effect in Haskell. Here's a variation without 'unsafeInterleaveIO': import Data.IORef import Control.Exception main = do r <- newIORef 0 let v = undefined handle (\(ErrorCall _)->print "hi">>return 42) $ case f v of 0 -> return 0 n -> return (n - 1) y <- readIORef r print y -- a couple of examples: f x = 0 -- program prints '0' f x = x -- program prints '"hi"0' (sideline: I often interpret '_|_::t' not so much as an element of 't' but as failure to produce information at type 't'; the type tells us what information we can have, evaluation not only provides the details, but also decides whether or not we have any of that info, and how much of it)

Furthermore, due to the monad laws, if f is total, then reordering the (x <- ...) and (y <- ...) parts of the program should have no effect.

case f v of { 0 -> return 0; n -> return (n - 1) } = return $! case f v of { 0 -> 0; n -> (n - 1) } =/= return $ case f v of { 0 -> 0; n -> (n - 1) } Monad laws apply to the latter, so how is reordering justified? It doesn't matter if 'f' is total, the context requires to know whether 'f v' is '0' or not. Since the only thing used from the result is its successful evaluation, the case could be eliminated, but that still leaves return $! f v =/= return $ f v

But if you switch them, the program will *always* print 0.

In my copy of the docs, the only things known about 'unsafeInterleaveIO' are its module, its type, and that is is "unsafe". If we assume, from the name, that evaluation of its parameter will be interleaved unsafely with the main IO thread, there is no knowing when or if that evaluation will happen. Unless there is a dependency on the result of that evaluation, in which case we have an upper bound on when the evaluation must happen, but still no lower bound. From the comments in the source code, it appears that lower and upper bound are intended to be identical, ie. evaluation is supposed to happen at the latest possible point permitted by dependencies. Changing dependencies changes the program.

Also, the compiller might notice that x is never used, and that "f" is total. So it could just optimize out the evaluation of "f v" completely, at which point the program always prints 0 again; changing optimization settings modifies the result of the program.

It doesn't matter whether or not 'x' is used. It matters whether 'f v' needs to be evaluated to get at the 'return' action. Even if 'f' is total, that evaluation cannot be skipped. Eta-expansion changes strictness, which changes the program (eg, '\p->(fst p,snd p)' =/= 'id::(a,b)->(a,b)', even though these functions only apply to pairs, so we "know" that "whatever 'p' is, it ought to be a pair" - only we don't; and neither do we know that 'f v' is a number, even if 'f' itself is total). None of this means that lazy IO and monadic IO ought to be mixed freely. If a program depends on strictness/non-strictness, that needs to be taken into account, which can be troublesome, which is why lazy IO hasn't been the default IO mechanism in Haskell for many years. It is still available because when it is applicable, it can be quite elegant and simple. But we need to decide whether or not that is the case for each use case, even without the explicit 'unsafe'. Hth? Claus

On Mon, 2009-03-16 at 22:12 +0100, Henning Thielemann wrote:

On Sun, 15 Mar 2009, Claus Reinke wrote:

...

import Data.IORef import Control.Exception

main = do r <- newIORef 0 let v = undefined handle (\(ErrorCall _)->print "hi">>return 42) $ case f v of 0 -> return 0 n -> return (n - 1) y <- readIORef r print y

I don't see what this has to do with strictness. It's just the hacky "exception handling" which allows to "catch" programming errors.

And which I have a sneaking suspicion actually *is* `unsafe'. Or, at least, incapable of being given a compositional, continuous semantics. jcc

On Mon, 2009-03-16 at 22:01 +0000, Duncan Coutts wrote:

On Mon, 2009-03-16 at 14:17 -0700, Jonathan Cast wrote:

...

On Mon, 2009-03-16 at 22:12 +0100, Henning Thielemann wrote:

...

On Sun, 15 Mar 2009, Claus Reinke wrote:

...

import Data.IORef import Control.Exception

main = do r <- newIORef 0 let v = undefined handle (\(ErrorCall _)->print "hi">>return 42) $ case f v of 0 -> return 0 n -> return (n - 1) y <- readIORef r print y

I don't see what this has to do with strictness. It's just the hacky "exception handling" which allows to "catch" programming errors.

And which I have a sneaking suspicion actually *is* `unsafe'. Or, at least, incapable of being given a compositional, continuous semantics.

See this paper:

"A semantics for imprecise exceptions" http://research.microsoft.com/en-us/um/people/simonpj/papers/imprecise-exn.h...

Basically if we can only catch exceptions in IO then it doesn't matter, it's just a little extra non-determinism and IO has plenty of that already.

I'm not sure that helps much. Given the following inequalities (in the domain ordering) and equations: throw "urk! " <= 1 evaluate . throw = throwIO evaluate x = return x -- x total catch (throwIO a) h = h a catch (return x) h = return x we expect to be able to reason as follows: throw "urk"! <= return 1 ==> evaluate (throw "urk!") <= evaluate 1 ==> catch (evaluate (throw "urk!")) (const $ return 2) <= catch (evaluate 1) (const $ return 2) while catch (evaluate (throw "urk!")) (const $ return 2) = catch (throwIO "urk!") (const $ return 2) = const (return 2) "urk!" = return 2 and catch (evaluate 1) (const $ return 2) = catch (return 1) (const $ return 2) = return 1 So return 2 <= return 1, in the domain ordering? That doesn't seem right. jcc

On Tue, 2009-03-17 at 01:16 +0000, Claus Reinke wrote:

...

...

...

...

"exception handling" which allows to "catch" programming errors. And which I have a sneaking suspicion actually *is* `unsafe'. Or, at least, incapable of being given a compositional, continuous semantics. "A semantics for imprecise exceptions" http://research.microsoft.com/en-us/um/people/simonpj/papers/imprecise-exn.h... Basically if we can only catch exceptions in IO then it doesn't matter, it's just a little extra non-determinism and IO has plenty of that already.

I'm not sure that helps much. Given the following inequalities (in the domain ordering) and equations: throw "urk"! <= return 1

Oops, left a superfluous return in there. I meant throw "urk!" <= 1 (The inequality is at Int).

...

==> evaluate (throw "urk!") <= evaluate 1

throw (ErrorCall "urk") <= evaluate (throw (ErrorCall "urk"))

Sure enough. But throwIO (ErrorCall "urk") /= _|_: Control.Exception> throwIO (ErrorCall "urk!") `seq` () ()

So that first step already relies on IO (where the two are equivalent).

Come again?

This is very delicate territory. For instance, one might think that this 'f' seems to define a "negation function" of information content

f x = Control.Exception.catch (evaluate x >> let x = x in x) (\(ErrorCall _)->return 0) >>= print

and hence violates monotonicity

(_|_ <= ()) => (f _|_ <= f ())

since

*Main> f undefined 0 *Main> f () Interrupted.

But that is really mixing context-free expression evaluation and context-sensitive execution of io operations. Most of our favourite context-free equivalences only hold within the expression evaluation part, while IO operations are subject to additional, context-sensitive rules.

Could you elaborate on this? It sounds suspiciously like you're saying Haskell's axiomatic semantics is unsound :: IO.

For instance, without execution

*Main> f () `seq` () () *Main> f undefined `seq` () ()

but if we include execution (and the context-sensitive equivalence that implies, lets call it ~),

So a ~ b = `The observable effects of $(x) and $(y) are equal' ?

we have

f () ~ _|_ <= return 0 ~ f _|_

so 'f' shows that wrapping both sides of an inequality in 'catch' need not preserve the ordering (modulo ~)

If f _|_ <= f (), then it seems that (<=) is not a (pre-) order w.r.t. (~). So taking the quotient of IO Int over (~) gives you a set on which (<=) is not an ordering (and may not be a relation).

- its whole purpose is to recover from failure, making something more defined (modulo ~) by translating _|_ to something else. Which affects your second implication.

If the odd properties of 'f' capture the essence of your concerns, I think the answer is to keep =, <=, and ~ clearly separate, ideally without losing any of the context-free equivalences while limiting the amount of context-sensitive reasoning required. If = and ~ are mixed up, however, monotonicity seems lost.

So catch (throwIO e) h ~ h e but it is not the case that catch (throwIO e) h = h e ? That must be correct, actually: Control.Exception> let x = Control.Exception.catch (throwIO (ErrorCall "urk!")) (\ (ErrorCall _) -> undefined) in x `seq` () () So catch is total (even if one or both arguments is erroneous), but the IO executor (a beast totally distinct from the Haskell interpreter, even if they happen to live in the same body) when executing it feels free to examine bits of the Haskell program's state it's not safe for a normal program to inspect. I'll have to think about what that means a bit more.

The semantics in the "imprecise exceptions" paper combines a denotational approach for the context-free part with an operational semantics

[Totally OT tangent: How did operational semantics come to get its noun? The more I think about it, the more it seems like a precís of the implementation, rather than a truly semantic part of a language specification.]

for the context-sensitive part. This tends to use the good properties of both, with a clear separation between them, but a systematic treatment of the resulting identities was left for future work.

jcc

...

So that first step already relies on IO (where the two are equivalent). Come again?

The first step in your implication chain was (without the return) throw (ErrorCall "urk!") <= 1 ==> evaluate (throw (ErrorCall "urk!")) <= evaluate 1 but, using evaluation only (no context-sensitive IO), we have

...

throw (ErrorCall "urk") <= evaluate (throw (ErrorCall "urk"))

Sure enough.

meaning that first step replaced a smaller with a bigger item on the smaller side of the inequation. Unless the reasoning includes context- sensitive IO rules, in which case the IO rule for evaluate brings the throw to the top (evaluate (throw ..) -> (throw ..)), making the two terms equivalent (modulo IO), and hence the step valid (modulo IO). Unless you just rely on

But throwIO (ErrorCall "urk") /= _|_: Control.Exception> throwIO (ErrorCall "urk!") `seq` () ()

in which case that step relies on not invoking IO, so it can't be mixed with the later step involving IO for catch (I think).

...

This is very delicate territory. For instance, one might think that this 'f' seems to define a "negation function" of information content

...

f x = Control.Exception.catch (evaluate x >> let x = x in x) (\(ErrorCall _)->return 0) >>= print

and hence violates monotonicity

(_|_ <= ()) => (f _|_ <= f ())

since

*Main> f undefined 0 *Main> f () Interrupted.

But that is really mixing context-free expression evaluation and context-sensitive execution of io operations. Most of our favourite context-free equivalences only hold within the expression evaluation part, while IO operations are subject to additional, context-sensitive rules.

Could you elaborate on this? It sounds suspiciously like you're saying Haskell's axiomatic semantics is unsound :: IO.

Not really unsound, if the separation is observed. One could probably construct a non-separated semantics (everything denotational), but at the cost of mapping everything to computations rather than values. Then computations like that 'f' above would, eg, take an extra context argument (representing "the world", or at least aspects of the machine running the computation), and the missing information needed to take 'f _|_'[world] to '()'[world'] would come from that context parameter (somewhere in the computational context, there is a representation of the computation, which allows the context to read certain kinds of '_|_' as exceptions; the IO rule for 'catch' takes that external information and injects it back from the computational context into the functional program, as data structure representations of exceptions). That price is too high, though, as we'd now have to do all reasoning in context-sensitive terms which, while more accurate, would bury us in irrelevant details. Hence we usually try to use context-free reasoning whenever we can get away with it (the non-IO portions of Haskell program runs), resorting to context-sensitive reasoning only when necessary (the IO steps of Haskell program runs). This gives us convenience when the context is irrelevant as well as accuracy when the context does matter - we just have to be careful when combining the two kinds of reasoning.

...

For instance, without execution

*Main> f () `seq` () () *Main> f undefined `seq` () ()

but if we include execution (and the context-sensitive equivalence that implies, lets call it ~),

So

a ~ b = `The observable effects of $(x) and $(y) are equal'

?

Observational equivalence is one possibility, there are various forms of equivalences/bi-similarities, with different ratios of convenience and discriminatory powers (the folks studying concurrent languages and process calculi have been fighting with this kind of situation for a long time, and have built up a wealth of experience in terms of reasoning). The main distinction I wanted to make here was that '=' was a context-free equivalence (valid in all contexts, involving only context-free evaluation rules) while '~' was a context-sensitive equivalence (valid only in IO contexts, involving both context-free and context-sensitive rules).

...

we have

f () ~ _|_ <= return 0 ~ f _|_

so 'f' shows that wrapping both sides of an inequality in 'catch' need not preserve the ordering (modulo ~)

If f _|_ <= f (), then it seems that (<=) is not a (pre-) order w.r.t. (~). So taking the quotient of IO Int over (~) gives you a set on which (<=) is not an ordering (and may not be a relation).

As I said, mixing '=' and '~', without accounting for the special nature of the latter, is dangerous. If we want to mix the two, we have to shift all reasoning into the context-sensitive domain, so we'd have something like f () [world] ~ _|_ [world''] <= return 0 [world'] ~ f _|_ [world] (assuming that '<=' is lifted to compare values in contexts). And now the issue goes away, because 'f' doesn't look at the '_|_', but at the representation of '_|_' in the 'world' (the representation of '_|_' in GHC's runtime system, say).

...

- its whole purpose is to recover from failure, making something more defined (modulo ~) by translating _|_ to something else. Which affects your second implication.

...

If the odd properties of 'f' capture the essence of your concerns, I think the answer is to keep =, <=, and ~ clearly separate, ideally without losing any of the context-free equivalences while limiting the amount of context-sensitive reasoning required. If = and ~ are mixed up, however, monotonicity seems lost.

So

catch (throwIO e) h ~ h e

but it is not the case that

catch (throwIO e) h = h e

? That must be correct, actually:

Control.Exception> let x = Control.Exception.catch (throwIO (ErrorCall "urk!")) (\ (ErrorCall _) -> undefined) in x `seq` () ()

So catch is total (even if one or both arguments is erroneous), but the IO executor (a beast totally distinct from the Haskell interpreter, even if they happen to live in the same body) when executing it feels free to examine bits of the Haskell program's state it's not safe for a normal program to inspect. I'll have to think about what that means a bit more.

Yes, exactly!-)

[Totally OT tangent: How did operational semantics come to get its noun? The more I think about it, the more it seems like a precís of the implementation, rather than a truly semantic part of a language specification.]

There's bad taste associated with the term, stemming from older forms of operational semantics that were indeed unnecessarily close to the implementations (well, actually, such close resemblance can still be useful to guide implementations, or to prove things about implementations, so there are many forms of operational semantics, varying in levels of abstraction to accommodate the target areas of study). Modern forms of operational semantics (when studying languages, not implementations) are much more abstract than that, closer to inference rules of a programming logic. Oversimplified: they study equivalence classes of semantics, using syntactic terms as canonical representatives. This use of syntax tends to confuse denotational semantics adherents, who say that syntax should be irrelevant in order to achieve sufficiently abstract semantics. But if we have two denotational semantics, S1 and S2, mapping constructs of language L to D1 and D2, respectively, then the only thing they are going to have in common are the constructs of L and, hopefully, the relations between the things these constructs are mapped to. So, if we want to abstract over the specific denotational semantics Sx, and its specific domain Dx, we just talk about [| L |] or, by abuse of notation, about L. So, when abstract operational semantics talk about 'X ~ Y' for some X,Y in L, they are really talking about 'forall semantics S :: L -> D. S[| X |]::D ~ S[| Y |]::D', without the repetitive details. In other words, when abstract operational semantics focus on syntax, they only focus on those aspects of syntax that are relevant to all semantics, such as composition and relations. Hey, who put me on that hobby-horse again?-) Claus

What does this mean again? I'm working on the assumption that `context-sensitive' means `under some (not necessarily compositional and/or continuous and/or monotonic) equivalence relation/

I'm using "contexts" as "expressions with holes", as used for "evaluation contexts" in operational semantics, where both contexts and expressions tend to be specified by grammars (in that form usually attributed to Felleisen, I think, though structural operational semantics often just group their rules into local reduction and congruence/embedding of reduction in subprograms) and rewrite rules and term relations can abstract over both expressions and contexts. For instance, if we have lambda calculus expressions E := v | \v.E | E E we can write arbitrary one-hole contexts as (where [ ] denotes the hole to be filled, and hole-filling is naive, not capture-avoiding) C[ ] := [ ] | \v.C[ ] | C[ ] E | E C[ ] and since we'd expect (using E1[E2/v] for capture-avoiding substitution of E2 for v in E1) beta-equivalence to hold in all contexts forall C v E1 E2. C[ (\v.E1) E2 ] =beta= C[ E1[E2/v] ] we usually abbreviate that as forall v E1 E2. (\v.E1) E2 =beta= E1[E2/v] So context-free rules are the subset of context-sensitive rules that neither limits, nor uses, nor changes the contexts in which the rule is applicable. A perfect match for purely functional evaluation. When we add IO, however, we add the ability for an expression to interact with the context it is running in, and that calls for the full range of context-sensitive rules. For instance, using monadic program contexts M[ ] := [ ] | M[ ] >>= E and some representation of context state, we can model monadic IO similar to communication in process calculi, with the functional program and its runtime context as parallel processes M[ getIO ] || Context[ char ] -getIO-> M[ return char ] || Context[ char ] and so on (see the Awkward Squad [0], Concurrent Haskell [1] and imprecise Exception papers [2] for Haskell-related examples; [0,1] use evaluation contexts, [2] uses separate structural and reduction rules).

The IO monad is still a part of Haskell's denotational semantics, right?

I believe you could make it so. But I suspect that a denotational semantics that covers both IO and functional evaluation would be more cumbersome to use than a hybrid semantics that treats functional evaluation denotationally and IO execution operationally. Which is why I'm with those who prefer the hybrid here. But then I'm definitely biased towards operational semantics in general, so others may offer different preferences on the same topic!-) Which reminds me of a useful encounter I once had with a non-functional, but thoughtful programming language person: I was going on about the greatness of purely functional programming and being able to replace equals with equals. He said something like this: "of course you can replace equals with equals - if you can't replace them, they can't be equal, right?-)" So, the real question is how useful the equality is, and the contexts in which you can do that replacing - after all, one can give denotational semantics for imperative languages as well.

Otherwise, I don't think we can really claim Haskell, as a language that includes IO in its specification, is truly `purely functional'. It's a language that integrates two sub-languages, one purely functional and one side-effectful and imperative. Which is a nice accomplishment, but less that what Haskell originally aimed to achieve.

[hobby-horse warning: see chapter 3 of [3], at least references in 3.6:-] Personally, I do indeed think that we should be talking about a pure, functional interactive language, not a purely functional one. There are two qualitatively different aspects of imperative functional programming languages, and trying to make one look like the other is obscuring the essential differences without being able to hide them completely. The early stream-based IO approaches were cumbersome, Clean's uniqueness-typed world passing approach is fairly clean, but at the cost of restricting functional code involved in IO (also, one still needs to interpret main :: *World -> *World as generating a _sequence of observable intermediate states_, unlike a "real" function applied to a single world, but similar to what a non-hybrid denotational semantics would have to do). I find Haskell's approach both simple (functional programs compute values, these values can include dialogues with the runtime context, dialogue values that reach the boundary between program and runtime context get interpreted as interactions between the two) and practical (there are lots of things from Clean that would be nice to have in Haskell, including uniqueness-typed environment passing as a safe basis for IO, but I'd still use monadic IO as an interface to that basis). Where does it say that Haskell aimed for anything else, btw?

I still don't understand what you're separating. Are you saying the semantics of terms of type IO need to be separated from the semantics of terms of non-IO type?

From the runtime environment perspective, functional evaluation creates

No. Yes. Well:-| There are really two aspects to the semantics of IO types: from the functional program perspective, they just contain certain abstract values, with certain abstract constructors, conforming to certain laws, nothing at all out of the ordinary. things of type IO, which get interpreted by the context, after which things repeat with modified context and modified functional program. So what needs to be separated are functional evaluation (under program control, context-independent) and program result interpretation (under runtime context control, context-sensitive). One can make the former part of the latter, but that makes things more complicated than they need to be; one shouldn't try to pretend that the latter is part of the former.

...

One could probably construct a non-separated semantics (everything denotational), but at the cost of mapping everything to computations rather than values.

So as long as Haskell is no longer pure (modulo lifting everything) it works?

That's the beauty of the non-lifted, hybrid approach: functional evaluation, including that involving IO types, remains pure, context-sensitive reasoning is limited to IO type interpretation, where it is unavoidable (interacting with the outside world is the purpose of IO, after all).

So I can't use normal Haskell semantics to reason about IO. That's *precisely* what I'm trying to problematize.

What semantics?-) But I agree that it is useful to point out those odd corners - all too often they get swept under the carpet (which then leads to panic when someone falls over one of those bumps that shouldn't be there, even when there usually is no problem if the formalization is precise).

...

The main distinction I wanted to make here was that '=' was a context-free equivalence (valid in all contexts, involving only context-free evaluation rules) while '~' was a context-sensitive equivalence (valid only in IO contexts, involving both context-free and context-sensitive rules).

That doesn't clarify anything, since what I'm trying to get clarified was the distinction you're making between `context-free' and `context-sensitive' reasoning.

Is that clearer now? If we have a Haskell program H running in parallel with other OS processes and services H || OS1 || ... || Keyboard || Screen then any functional evaluation inside H is completely independent of the context in which H is executing (modulo asynchronous exceptions, stack overflow, someone switching off the computer). When we reason about such functional evaluation, we can completely ignore that there even is such a context. Whenever H engages in IO, however, we need to reason in a way that involves both H and its runtime context, so our reasoning becomes context-sensitive. It just so happens that this difference corresponds to the difference between context-free and context-sensitive rewriting in operational semantics, so I'm not always distinguishing between the physical and the modeled contexts. While I believe my preference to be based on real benefits, it is a personal preference - there are other ways to capture the same issues, including the use of continuation-passing style to enable functional programs to abstract over contexts as well as over values.

...

...

So catch is total (even if one or both arguments is erroneous), but the IO executor (a beast totally distinct from the Haskell interpreter, even if they happen to live in the same body) when executing it feels free to examine bits of the Haskell program's state it's not safe for a normal program to inspect. I'll have to think about what that means a bit more. Yes, exactly!-) OK, so I got one thing right.

Isn't that the essence of this thread? Everything else follows from there (well, plus the fact that strictness is part of a program's semantics, not just an artifact of the implementation).

...

[machine-level vs language-level operational semantics] Can you point me in the direction of some examples of this contrast? Not just because I'd like to understand it, but because at some point I should really produce an operational semantics for Global Script, and I'd like to follow the best style here.

Best style depends on your purpose - if it makes the ideas you find important clear, go with it, and if you have more problems with the notation than with the ideas you want to think about, the notation isn't right for you, no matter what others have used for their problems!-) But it couldn't hurt to look at, say, Olivier Danvy and coworker's publications at BRICS[4]: they have been rather thorough in documenting various semantics folklore, including formal derivations of abstract machines from operational semantics and correspondences between various forms of operational semantics. Such derivations are usually easier than trying to prove equivalence of separately developed semantics and implementation. Gordon Plotkin's notes and references are certainly relevant [5]. Also check out the several treatments of lazy lambda calculus and call-by-need reduction: the earliest ones relied on a combination of language-level rules with an abstract heap to model sharing, the later ones represent sharing entirely at the language level[6].

...

Oversimplified: they study equivalence classes of semantics, I thought in a fully-abstract denotational semantics we had [| x |] = [| y |] whenever x and y were operationally equivalent?

And if you have that, doesn't that imply that everything else about the denotational semantics is irrelvant? In particular, any denotational semantics that includes things not present in the operational one, or vice versa, is not fully abstract. Claus [0] Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell, Simon Peyton Jones http://research.microsoft.com/en-us/um/people/simonpj/papers/marktoberdorf/ [1] Concurrent Haskell, Peyton Jones, Gordon, Finne http://research.microsoft.com/en-us/um/people/simonpj/papers/concurrent-hask... [2] A semantics for imprecise exceptions, Peyton Jones, Reid, Hoare, Marlow, Henderson http://research.microsoft.com/en-us/um/people/simonpj/papers/imprecise-exn.h... [3] Functions, Frames, and Interactions, Claus Reinke (chapter 3) http://www.cs.kent.ac.uk/~cr3/publications/phd.html [4] Olivier Danvy et al, miscellaneous reports http://www.brics.dk/~danvy/ [5] The Origins of Structural Operational Semantics, Gordon D. Plotkin, number 48 here: http://homepages.inf.ed.ac.uk/gdp/publications/ [6] A call-by-need lambda calculus, John Maraist, Martin Odersky, and Philip Wadler http://homepages.inf.ed.ac.uk/wadler/topics/call-by-need.html#need-journal A natural semantics for lazy evaluation, John Launchbury http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.35.2016&rep=rep1&type=pdf

On Tue, 2009-03-17 at 12:59 +0100, Ketil Malde wrote:

Duncan Coutts writes:

...

...

[..] I have a sneaking suspicion [exceptions] actually *is* `unsafe'. Or, at least, incapable of being given a compositional, continuous semantics.

...

Basically if we can only catch exceptions in IO then it doesn't matter, it's just a little extra non-determinism and IO has plenty of that already.

Couldn't you just substitute "catch exceptions" with "unsafePerformIO" here, and make the same argument?

This puzzled me, until I realized you meant `unsafeInterleaveIO'. That's pretty much the argument that is made for unsafeInterleaveIO.

Similarly, can't you emulate unsafePerformIO with concurrency?

Assuming you mean unsafeInterleaveIO, not quite. GHC's scheduler is fair, so you are guaranteed after forkIO $ a that a's side effects will happen eventually. On the other hand, after unsafeInterleaveIO $ a you have basically no guarantee the RTS will ever get around to scheduling a. (In fact, if you write it just like that in a do block, rather than saying x <- unsafeInterleaveIO $ a you are pretty much guaranteed that the RTS won't ever feel like scheduling a. It'll even garbage collect a without ever executing it.)

Further, couldn't you, from IO, FFI into a function that examines the source code of some pure function, thus being able to differentiate funcitions that are normally "indistinguishable"?

Regular IO is good enough for this.

I've tried to follow this discussion, but I don't quite understand what's so bad about unsafeInterleaveIO - or rather, what's so uniquely bad about it. It seems the same issues can be found in every corner of IO.

jcc

On Sun, 15 Mar 2009, Ryan Ingram wrote:

unsafeInterleaveIO allows embedding side effects into a pure computation. This means you can potentially observe if some pure value has been evaluated or not; the result of your code could change depending how lazy/strict it is, which is very hard to predict!

For example:

...

-- given f :: Integer -> Integer

main = do r <- newIORef 0 v <- unsafeInterleaveIO $ do writeIORef r 1 return 1 x <- case f v of 0 -> return 0 n -> return (n - 1) y <- readIORef r print y

-- a couple of examples: f x = 0 -- program prints "0" -- f x = x -- program prints "1"

Interesting example. I have implemented the lazyio package. It asserts that unsafely interleaved IO actions are performed in order. This should prevent such problems, does it? However, they are only avoided within the LazyIO monad. Running the LazyIO monad in IO allows the same corruptions as shown above. http://hackage.haskell.org/cgi-bin/hackage-scripts/package/lazyio

Hi, On 2009/03/16, at 10:04, wren ng thornton wrote:

...

next r = do n <- readIORef r writeIORef r (n+1) return n

Now, if I use unsafeInterleaveIO:

...

main = do r <- newIORef 0 x <- do a <- unsafeInterleaveIO (next r) b <- unsafeInterleaveIO (next r) return (a,b) ...

The values of a and b in x are entirely arbitrary, and are only set at the point when they are first accessed. They're not just arbitrary between which is 0 and which is 1, they could be *any* pair of values (other than equal) since the reference r is still in scope and other code in the ... could affect it before we access a and b, or between the two accesses.

OK, the values of a and b depend how to deconstruct x.

Moreover, let's have two pure implementations, f and g, of the same mathematical function. Even if f and g are close enough to correctly give the same output for inputs with _|_ in them, we may be able to observe the fact that they arrive at those answers differently by passing in our x. Given that such observations are possible, it is no longer safe to exchange f and g for one another, despite the fact that they are pure and give the same output for all (meaningful) inputs.

Hm, Does it means that in optimization, a compiler may replace implementation of a pure function that have different order of evaluation, so order of actions would be different in some environments?

On Monday 16 March 2009 2:11:10 pm Ryan Ingram wrote:

However, I disagree with your description of what "unsafe" should be used for. "unsafe" calls out the need for the programmer to prove that what they are doing is safe semantically, instead of the compiler providing those proofs for you. Whether that is due to type safety (unsafeCoerce) or breaking the assumptions of the compiler (unsafePerformIO, unsafeInterleaveIO, unsafeIOToST), depends on the situation.

Of course, unsafeIOToST can also break the type system, because you can write: unsafePerformIO m = runST (unsafeIOToST m)

For example, unsafePerformIO can make your program not type-safe, but it's convoluted to do so; in fact, at monomorphic types it can't break type safety. That's not what makes it unsafe at all. It's unsafe because it breaks the rule that pure values don't have side effects, so that the effects inside the unsafePerformIO might get executed more than once, or not at all, depending on how the compiler decides to evaluate the pure value returned. And what happens could depend on the optimization settings of the compiler, the timing of the machine you are running on, or the phase of the moon.

In practice, 'unsafe' can mean any number of things depending on the context. unsafeRead/Write on mutable arrays can (attempt to) read/write arbitrary memory locations. An index into a data structure that just calls error instead of returning a Maybe result might be called unsafe. In a similar vein, some people think head and tail should be called unsafeHead and unsafeTail. :) Technically, one can probably lay down a semantics of IO such that unsafeInterleaveIO maintains the purity of the language by the usual definitions. However, such a semantics is necessarily too vague to explain why you might want to use it in the first place, because the only real reason you'd want to do so is to have side effects triggered in response to evaluation of otherwise pure terms. At the very least, using unsafeInterleaveIO adds significant complications to reasoning about the behavior of otherwise ordinary IO, which might well justify its name. -- Dan