[TYPES] The type/object distinction and possible synthesis of OOP and imperative programming languages

[Neelakantan R. Krishnaswami]

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.

Hi Greg,

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.

-- Neel

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.