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

[Mark Miller]

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, like caretakers and membranes. A partial
answer is Paritosh's first-class match types/functions, most of whose
benefits can be obtained using GADTs, as Pari explains at
<http://lambda-the-ultimate.org/node/1635#comment-20128>. (GADTs are
"generalized algebraic data types", available in some versions of
Haskell) IIUC, Pari's techniques should enable a statically typed
caretaker.

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.

By "fully static", I'm exempting systems like Java and Joe-E, where
there's an escape to a generic dynamic type (object) and so-called
reflection for operating on dynamically typed objects. Using this
escape hatch, membranes and other access abstractions (like Horton)
can still be expressed in these languages without wrestling with the
type system.


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


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

    Cheers,
    --MarkM