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

[Mark Miller]

On Dec 13, 2007 11:55 AM, Jonathan S. Shapiro <shap at eros-os.com> wrote:
> > > 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.


Ok, now I think I mostly understand the question. Except that the
question I think I understand would convert from a received byte
sequence to an typed object by safe unserialization, not upcasting.
This raises the question of how one can write a statically typed safe
unserializer. As Jonathan Rees first pointed out to me,
unserialization can be viewed as a simplified form of eval(). (Data-E
is based on this idea.) GADTs are sufficient to write a statically
typed eval(), and so should be sufficient to write a statically typed
safe unserializer.

Does this answer the actual question?

-- 
Text by me above is hereby placed in the public domain

    Cheers,
    --MarkM