On Tue, 2009-03-17 at 12:40 +0000, Claus Reinke wrote:
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.
And the larger side! I'm trying to determine whether there can exist a denotational semantics for IO, which treats it as a functor from (D)CPOs to (D)CPOs, for which the corresponding denotational semantics for the IO operations satisfies the requirement that they are both monotone and continuous. So I assumed monotonicity of evaluate.
Unless the reasoning includes context- sensitive IO rules,
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/
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).
The IO monad is still a part of Haskell's denotational semantics, right? 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.
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.
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?
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?
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).
So I can't use normal Haskell semantics to reason about IO. That's *precisely* what I'm trying to problematize.
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).
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.
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.
What is the special nature? What does ~ actually mean? You haven't actually specified that yet.
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!-)
OK, so I got one thing right.
[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.
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.
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?
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.
That makes sense. (Although I'm a big fan of repetitive details --- I use m// and q{} in Perl, (usually) even when there's no real need to --- so I'd probably end up actually saying [| X |] ~ [| Y |] anyway. Provided I understood precisely what that meant).
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?-)
*hides* jcc