[Prev][Next][Index][Thread]
RE: Abstraction Power
Hi Peter:
I don't have Reynolds's paper handy, but if I interpret your summary
correctly you're suggesting to use what amounts to a substitution
interpretation of free variables, then "abstract" by letting a (closed)
lambda denote a set of pairs. The existential encoding simply amounts to
delaying the substitution; it's the type system you need to correctly
express the delaying, without resort to ad hoc primitive mechanisms that
would amount to particular instances of existentials. Or did I miss your
point? It seems to me that the analysis in terms of existentials does
"explain" procedural abstraction as data abstraction. What is missing?
The connection with Pierce-Turner is to view a function as an object
with one instance variable (the environment) and one method (the function
body). This analogy is the more vivid when you consider clusters of
mutually recursive functions, which are not separable from one another.
Then you get one instance variable (the environment) and multiple methods
(the functions). In a more refined analysis you can also "explode" the
environment to get one instance variable per environment entry. As in the
original Pierce-Turner paper imperative aspects are not modelled; so-called
"functional" objects are interesting without mutation, despite the fact that
all "real" oopl's rely heavily on mutation. Again I see this explanation of
(recursive) functions as (functional) objects as completely satisfactory,
and am puzzled by what I'm missing. To me they are precisely the same
notion. One possible difference, however, is that in an oop framework you
are given a handle on the entire cluster of recursive functions (ie, "this"
or "self"), whereas in typical treatments of functions you get a handle only
on the individual functions within the cluster. However, by a kind of eta
expansion you can recover the cluster from its components, so I'm not sure
there's a huge difference here.
Regarding "extrusion", I'm not sure I understand the point, but
perhaps the issue you're concerned with is the difference between pure
existentials and the variant existentials that Lillibridge and I devised in
connection with our study of the type theory of module systems. Pure
existentials have a scoped elimination form "open p as t, x:tau in e end",
where e is the scope of the abstraction. It is essentially impossible to
allow t to "escape its scope", which significantly limits the utility of
pure existentials. Our approach is to drop "open" as the elimination form
in favor of "dot notation". Given a package value pv you can refer to its
type component as type(pv) and its implementation component as impl(pv); the
restriction to values is essential on for type(pv), incidentally.
Abstraction is preserved (unlike substitution-based formalisms derived from
strong sums), and it is possible to pass around values of abstract type
without worrying about the scope of the abstraction. This is what makes it
more powerful than "open", and different from strong sums. Moreover, the
dot notation is compatible with dependent types, which are required to
manage sharing specifications as are found in ML. I'm not certain if this
answers your question, but it might. I'd be interested to hear what you
think.
Finally, regarding imperative objects and issues of sharing that
arise in such formalisms, I don't have much to say. The point is that in a
purely functional setting recursive functions and functional objects are the
same notion, and both are adequately and accurately modelled using
existentials.
Best,
Bob
-----Original Message-----
From: Peter O'Hearn [mailto:ohearn@dcs.qmw.ac.uk]
Sent: Saturday, January 08, 2000 3:15 PM
To: Greg Morrisett; types@linc.cis.upenn.edu
Cc: ohearn@hotpoint.dcs.qmw.ac.uk
Subject: RE: Abstraction Power
[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
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.
Follow-Ups: