[cap-talk] Access Abstraction vs Static Typing (was: David Wagner's Google techtalk is now up!)

[Jonathan S. Shapiro]

On Thu, 2007-12-13 at 11:39 -0800, Mark Miller wrote:
> On Dec 13, 2007 10:57 AM, Jonathan S. Shapiro <shap at eros-os.com> wrote:
> > On Thu, 2007-12-13 at 13:38 -0500, Jonathan S. Shapiro wrote:
> > > There are
> > > real restrictions that a safe static type system imposes. One, which
> > > MarkM can explain better than I, is that static types and first-class
> > > messages are not really compatible (more precisely: first class reply
> > > messages) within the current state of the art of type theory.
> 
> The conflict between types and first class messages isn't specific to
> the I/O boundary. It's an issue that comes up when writing many
> generic access abstractions...

Yes. What I was wondering was whether dynamic checked upcast, which
works to solve one of those problems (I/O) might not be sufficient
pragmatically to deal with the other (messages).

> Another part of the puzzle is highlighted by the incredible degree of
> difficulty that the static typing aficionados on LtU had expressing a
> statically typed membrane
> <http://lambda-the-ultimate.org/node/1625#comment-19906>. Although
> they did ultimately succeed, the difficulty they encountered and the
> obscurity of the result, to my mind, disqualified fully static type
> systems from being ready for practical use. If it's this hard doing a
> simple membrane, good luck doing Horton.

I can't say that I like that conclusion, but it is extremely useful to
have a simple challenge problem like this whose pragmatic utility is
relatively easy to see.

> > A bit of follow up on this. Recently, Scott Smith, Swaroop, and I were
> > discussing the typed I/O problem, and the apparent need for checked
> > dynamic upcast in any sensible static language. We identified a set of
> > criteria under which the result of a checked upcast may alias the
> > untyped (really: vector of bytes) state originally delivered by the I/O
> > system.
> >
> > Granting that this is not a fully static check, my question to MarkM is:
> > would the first-class reply message issue be sufficiently resolved (in a
> > pragmatic sense) by treating the low-level reply as a vector of
> > characters and using checked upcast to get out the appropriate reply
> > type?
> 
> I don't understand the question. How did "vector of characters" enter
> the discussion?

Sorry. Should have written "vector of bytes". What I was trying, badly,
to express is that there is some level of abstraction where all messages
can be viewed as byte sequences, so vector of bytes becomes an awkward
sort of universal type from which checked upcasts can be performed.  I
think I was trying to express something similar to the role of Object
and introspection that you cited for Java. The reason I was thinking in
terms of vector of bytes was probably that I started coming at the
problem from the direction of the primitive I/O interface.

shap