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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe