[Prev][Next][Index][Thread]
RE: Abstraction Power
> 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:
t1 -> t2 = Exists t . ( t * ([t,t1] -> t2) ]
That is, a closure is a pair consisting of an environment (t) and
a piece of code. The code takes the environment and argument (t,t1)
and produces a result (t2). The type of the environment must
be abstracted because:
(a) different closures with the same type may have different
types for the environment:
if tuesday() then
let x = 3 in (fn y:int => y + x)
else
(fn z:int => z)
In the example above, the first function will have an
integer in the environment whereas the second function
will not.
(b) the only access that the outside world should have for the
environment is to pass it to the code for the closure.
This is how Bob Harper, Y. Minamide, and I formulated "typed closure
conversion" back in PoPL'96. The intention then was to model what
goes on in real functional language compilers. But in hindsight, it
very precisely connects abstraction via procedure with abstraction
via types. And of course, this also connects with simple object
systems in that the above interpretation is a special case of
the Pierce-Turner object encoding where we have one method.
So, certainly at a typed intermediate language level, simple
closed-scope user-level ADTs (i.e., existentials), closures,
and simple objects are the same. Matthias's defstruct can
be interpreted in a similar (but dynamic) fashion.
-Greg