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

Hi Bob,

I simply mean a standard denotational model, where a term denotes a function
from environments to values. The point is that I think it's the step to the
set of pairs (values as functions), and not
delaying or otherwise working with the environment, that has essentially
to do with abstraction. Your encoding is really silent on that, which is
not to say incompatible.

In particular, your remarks above
have only to do with delaying substitutions, which is all well and good,
but which appears to me to have nothing to do with the abstraction part of
procedural abstraction. You say to me: what is missing? I may be being thick,
and don't mean to patronize, but I would have to ultimately respond:
what is there (that has to do with procedural abstraction)?

I guess part of it might be that in
  A->B  ==>   Exists X. X x (A->B)
you still have to explain the -> on the right, where much abstraction
still resides. Note that I'm not saying that's exactly the problem: it's up
to you to explain how the encoding explains abstraction, if it does.

BTW, I gave the functional language example only as an *example*, as I wouldn't
want to focus on purely functional languages, and the function semantics
that goes with it. And neither do I claim that a denotational model
is *necessarily* the only way to explain abstraction; you may prefer
something else. But it is clear that denotational models are exceptionally
simple and direct, for this purpose, independently of whatever other
approaches one might come up with.


>Again I see this explanation of
>(recursive) functions as (functional) objects as completely satisfactory,
>and am puzzled by what I'm missing.

Well, I don't know either. You appear to be reacting to my statement


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

but I had prefaced that with talk about state: the remark was not about
purely functional objects. I don't disagree with what you say about
functional objects, and perhaps there was typically different understanding
of terms when you reacted to my point: I never feel the need to qualify
"object" with "imperative", so wasn't saying anything about functional
objects!  But,
I must add  that I have a very hard time seeing how functional objects are
interesting (except as a "theoreticians playpen" notion for studying type
systems).


>
>	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.
> ...
>   I'm not certain if this
>answers your question, but it might.  I'd be interested to hear what you
>think.

Thanks for the pointer.  It doesn't answer my question yet, without a lot
more analysis from someone; I'll certainly have a look.

best wishes, Peter
References: