[TYPES] The type/object distinction and possible synthesis of OOP and imperative programming languages
Neelakantan R. Krishnaswami
neelk at mpi-sws.org
Fri Apr 19 16:17:56 EDT 2013
On 04/19/2013 07:25 PM, Greg Morrisett wrote:
> [ The Types Forum,
> http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>> I disagree that ADTs are equivalent to either modules or objects.
>> Read Cook's essay for a discussion of the latter; for the former,
>> consider that it's often useful to define more than one ADT in a
>> single module.
> That's why I said "degenerate case". Modules, as strong sums, are
> more general. Objects are excessively narcissistic because they are
> fundamentally restricted to weak sums.
I don't understand your point. Weak sums, strong sums, and
functional objects seem strictly incomparable.
Weak sums ∃α.A(α) have an equality principle that lets you choose
different representation types for equal packages pack(A,e) and
pack(B,t), as long as you can give a relation between A and B that is
preserved by e and t.
OTOH, strong sums Σα.A(α) don't support this principle,because if you
have e = t : Σα.A(α), then you know that fst(e) = fst(t), implying that
the representation types of equal elements must be equal.
Functional objects are different again. They are typically described as
recursive records – that is, interface types like μα.A(α) where A
is a record of methods. If you try to convert such a recursive type to
an existential, you'll get ∃α. α × (α → A(α)), which is a very
different type from ∃α.A(α).
It's not only different because of the hidden state, but also because
object types need fully general recursive types with negative
occurrences (e.g., a distance function on a Point type which takes
another Point as an argument). If you attempt to model this with
one of the usual encodings in System F:
μα.F(α) ≜ ∀α. (F(α) → α) → α
να.F(α) ≜ ∃α. α × (α → F(α))
with a mixed-variance F, you don't get the recursive type you'd
expect, and so it seems to me you can't encode functional objects.
P.S. Imperative objects seem different yet again, since many imperative
OO designs (like the subject-observer pattern and MVC) rely on very
wild aliasing, and reasoning about them has a rely/guarantee flavor.
More information about the Types-list