[Haskell-cafe] What unsafeInterleaveIO is unsafe

[Jonathan Cast]

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