[Prev][Next][Index][Thread]
RE: Abstraction Power
Greg, I found your note both baffling and intruinging...
------
>
>> User-defined types and procedural data structures as complementary
>> approaches to data abstraction.
>
>One way to easily see that procedures (more properly closures)
>provide for "generative" data abstraction is to view closures
>more primitively as existentials:
I don't see how your encoding helps to "easily see" procedural data
abstraction.
For example, in the referenced paper "User defined..."
a purely functional language is used, and one can give that
language a very satisfactory semantics using (mathematical) functions,
where a lambda-abstraction denotes a function. Then, "procedural abstraction"
is explained perfectly by the set of pairs that a term denotes,
which abstracts from all internal details.
And in that paper procedure-based data abstraction is done essentially
by reducing to procedural abstraction, or using it in a stylized way. Now,
in the semantics I just mentioned you do use environments to structure the
semantic equations, but they disappear in the final values of the terms: I
don't see how
the existential encoding could improve upon it.
More generally, though, it seems to me that your encoding is describing
the way environments work using type-based data abstraction, but is not
*explaining* procedural data abstraction. You said
> The intention then was to model what
>goes on in real functional language compilers.
and then
>But in hindsight, it
>very precisely connects abstraction via procedure with abstraction
>via types.
I guess I get the first part, but not the second; at least, you don't
explain procedural data abstraction with type quantification (as far
as I can see).
-----
Nonetheless, there *is* the long-standing analogy between objects and
closures: it's fascinating that you use the same mechanism as in the
Pierce-Turner
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? Well, an object can certainly be implemented as a
closure, 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.
Regarding objects and state, there are two problems.
First, Pierce and Turner (and later, Hofmann) use their encoding
to interpret purely functional objects, where the "state" is not really
state. There is of course the destructive aspect of state, but even more
important is the fact that the distinction between copying and sharing
becomes relevant: I don't see any way of using the given existential
encoding to deal with sharing, where sending an object to a client
causes the local state of another object to be updated. Of course,
one could take an imperative target language for the encoding, but this
would be cheating: the existential encoding would be good for typing
(as was entended), but would not explain the "hidden" aspect of hidden state.
At least, that's the way I understand it: I'd be very happy, of course, if
someone could show me wrong, by giving a convincing existential encoding of
an OO language with state. But I expect that the encoding would have to
be altered in ways that would make it different from your treatment of
closures. In fact, Bob Tennent, John Reynolds and I have explored the link
between type quantification and hidden local state in a series of
papers (POPL93,JACM95,JACM2000), and used encodings that were related
to, but different from, the Pierce-Turner encoding. The differences had
mainly to do with the need to account for sharing.
The second problem is perhaps more significant: extrusion. In an OO
language it is crucial to be able to pass the identity of an object
(often yourself) to another object, which may then store this identity, as in
the classic "listener" idiom.
(Semantically, this is like storable procedures.) The problem
is that extrusion allows a locally-declared reference or object to "leak"
from a local context, in a way that does not seem to be analogous to anything
that can be done with type quantification (Again, I'd be happy to
be shown wrong). Since extrusion is so fundamental
in OOP (it even forms the basis of Hewitt's actor model), this makes
me doubt whether the "hiding" acheived using type quantification is
the same as the hidden local state found in objects (or Scheme or ML,
for that matter). "Doubt" here means I don't know if they're
the same or different, even though for neatness I wish they were the same.
I recently wrote a survey article for SIGACT
ftp://ftp.dcs.qmw.ac.uk/lfp/ohearn/sigact.ps
discussing some of these ideas and problems:
the problems have not been resolved yet, as far as I am aware.
Anyhow, I hope you can see why I was *both* baffled and intruiged by your
message.
best wishes, Peter
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.