RE: Abstraction Power
> More generally, though, it seems to me that your encoding is
> the way environments work using type-based data abstraction,
> but is not
> *explaining* procedural data abstraction.
Fair enough. Perhaps I should've said something like: This
particular encoding explains an implementation-oriented
connection between simple abstract data types and procedural
abstraction in a purely functional setting. Namely, when
procedures are viewed as closures -- pairs of *closed* code
and an environment, we must use some other mechanism to obtain
abstraction than partial applications. Existential types provide
an appropriate mechanism.
Another way to say this, is that the arrow type "t1 -> t2"
hides the typing assumptions from the context:
A, x:t1 |- M : t2
A |- \x:t1.M : t1->t2 (A doesn't show up in result type)
In a setting where we have only *closed* code (let me write t1=>t2 for
closed functions from t1 to t2), then typing assumptions
by necessity show up in the type, as in:
X:T, x:t1 |- M : t2
|- \[X:T,x:t1].M : T*t1=>t2 (all assumptions show up in type)
To translate open terms (->) to closed ones (=>) requires that we make
the context explicit. Doing so in a straightforward fashion is not
type-preserving -- we must explicitly abstract the assumptions,
whereas "->" hides these assumptions implicitly. Hence the translation
[t1->t2] = Exists T.(T * ((T * [t1]) -> [t2]))
Indeed, if you have the "whole" program, you can replace the existential
(as infinite sum) with a finite sum, appropriate injections and case
This is the "defunctionalization" that Reynolds did and others
followed up on. However, it's far more context-sensitive.
> Nonetheless, there *is* the long-standing analogy between objects and
> closures: it's fascinating that you use the same mechanism as in the
> encoding. But I'm still baffled (generally, not by the
> specifics of your paper)
> about several things. First, you use type quantification
> to hide the environment, where Pierce-Turner use it to hide state,
> but the environment and the state are not the same. So, how
> good is the
> analogy between objects and closures, and how well is it
> expressed formally
> using existentials?
It turns out that if you have a language where objects may be
nested, then you have to "closure convert" your objects in an
implementation -- that is, account for the free identifiers of
the environment -- a similar sort of encoding goes on here.
See Neal Glew's HOOTS'99 paper for an example.
But you're right -- the encoding gives no insight into the
issues of state or identity.
> Well, an object can certainly be implemented as a
Only very simple forms of objects. Encodings such as the
ones provided by Kim Bruce, or Abadi and Cardelli, or
Viswanathan et al. show the need for some form of recursion
in the types to achieve a suitable encoding.
This is also true for recursive functions, though the details
are not quite the same. Bob Harper and I wrote another note
for HOOTS (98?) where we showed that each of the standard object
encodings could be used for recursive function encodings but that they
tended to be overkill. Unlike objects, there's no need for
things like method override, identity, etc. Interestingly,
an encoding showed up that isn't discussed in the object
literature that much, but seemed (to me) to be the most
appropriate one for (mutually) recursive closures.
> but it also involves hidden state, and I'm not
> convinced that this
> "hidden state" aspect is properly captured by the
> Pierce-Turner encoding,
> except in
> extremely contained laboratory conditions. So, I don't yet
> see that the
> link of your work and Pierce-Turner is really
> a *completely* satisfactory expression of the longstanding
> analogy between
> objects and closures.
Yes -- of course state throws a major monkey wrench into
everything. When I said "simple object", I was throwing out
state, method override, and a host of other things that you
> P.S. I did notice that you were careful to qualify "object"
> with "simple"
> on several occasions, presumably ruling out "complex" objects (with
> extrusion, sharing)... so, I realize that this last bit does
> not contradict
> anything you said.
I should've been more careful -- I wasn't trying to claim anything
deep or new, rather that I found the closures as existentials a
nice way to explain a connection between abstract data types and