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

[Greg Morrisett]

> I don't understand your point.  Weak sums, strong sums, and
> functional objects seem strictly incomparable.

Yes, I shouldn't have used strong and weak.  Rather, in most
OO languages (and with the simple version of Haskell type classes)
there is a unique type specified implicitly in the interface ("self").
This is the narcissism that I was referring to. Whereas, with modules,
it's common to define multiple types in the interface (e.g., the type of
maps, and the type of their keys and values.)  In Haskell, we
hack around this with associated types, functional dependencies
and the like.  It's much cleaner to just have multiple type
definitions and true dependency (as well as computation at the
type level.)

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

I didn't mean to suggest you don't want weak sums.  (I am a huge
fan.)

> 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(α).

Neel, I remember all of this stuff from the 80s-90's
quite well.  See my papers relating these to closure
compilation techniques with Harper --- I do find the
Pierce-Turner pattern:

   ∃α. α × (α → A(α))

or a la Haskell:

    ∃α. C α => α

which is the essence of a closure, works extremely well in
many situations where I want a heterogeneous
collection.  I particularly like that I can choose where
to put that existential and class constraint so I can
choose to have e.g.,

   ∃α. C α => Set α

and factor out the method table for a whole collection.
So unlike Jonathan, I find this control crucial, and don't
seem to mind the price of the wrap/unwrap.

As you noted, it doesn't work well when trying to perform
operations *across* values (unless we've abstracted the
type over a collection as I did above.)  But the usual
solution is to provide conversions to a common representation
(e.g., provide a to_cartesian for your point interface,
and then implement the distance operation using this
method.)  I'm not sure it works well in e.g., Java either
without resorting to something like this.

-Greg