[gclist] Re: buffer example

[David Petrie Stoutamire]

Hans:

I conceed that in order to guarantee that the buffer is flushed before
closing the output stream, there is an order dependence that requires
violating the original abstraction; by modifying the output stream
implementation, using pointer ordering or by some other hack.

One thing that interests me about this example is that there's a sense
in which the buffered output stream abstraction is broken even if
finalization isn't involved.  Since the output stream has an explicit
close operation in addition to finalization, it is possible to manually
break the buffered stream by closing the output stream it is using.

Clearly this is a violation of `exclusive use'.  How is exclusive use
guaranteed?  Typically by having the buffered stream create the output
stream and never giving a pointer to it out.  Finalization is breaking
the intended exclusive use by invoking an operation that wasn't
initiated by the buffered stream itself.

This is interesting because there are languages that could express this
notion of having the exclusive reference on which the buffered stream
depends.  I'm thinking of linear types or Mercury unique modes (I
wouldn't be surprised to learn of others).  The presence of a
finalization operation would violate such a unique-reference assertion
on that type, making the (broken) buffered stream impossible to
express, or at least pointing the problem out statically.

Fergus, if you are reading this, what does Mercury say about
finalization and unique modes?

    - Dave

--
David Stoutamire
http://www.icsi.berkeley.edu/~davids