[Haskell-cafe] What unsafeInterleaveIO is unsafe

Thu Mar 19 22:30:54 EDT 2009

> 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?

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.

>From the runtime environment perspective, functional evaluation creates 
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-haskell.ps.gz
[2] A semantics for imprecise exceptions, Peyton Jones, Reid,
    Hoare, Marlow, Henderson
    http://research.microsoft.com/en-us/um/people/simonpj/papers/imprecise-exn.htm
[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