Lambda the Ultimate

...and as others have pointed out elsewhere, it sounds an awful lot like Cyclone, which you can download and use today.

Subtype polymorphism (which he calls "inheritance", although inheritance is one of many ways to implement subtyping)

But he is really comparing inheritance - this is important to note, because some of his main arguments have nothing to do whatsoever with subtyping (in particular, dynamic dispatch).

The fact that he does not properly distinguish here (which probably would be a bit much to expect from a '86 paper) implies that his conclusions have to be taken carefully.

His conclusion? Subtype polymorphism is "better" because it can simulate generic polymorphism, although in a type-unsafe manner.

Excuse some lecturing, but...

Stated this way the claim is a non-sequitur. Anything can certainly be simulated "in a type-unsafe manner". So you have to refine that statement to restrict type-unsafe operation to down-casts.

But then you still make at least two silent assumption: first, that there is a Top type ("Object" or whatever) in your subtyping hierarchy, which is not necessarily the case (e.g. C++). And second, that you actually have down-casts, which is not necessarily the case either (e.g. OCaml), and certainly not a defining property of subtyping.

Obviously, with Top and down-casts, you can make a program almost completely untyped, which brings us back to the first point. So you want to restrict the statement further to allowing only "certain" uses of down-casts. How to qualify these is non-obvious.

Now, even considering these important restrictions the statement is nonsensical, because "polymorphism" is a type system property, and it does not make the least sense to say you "simulate" a type system feature in a "type-unsafe" way.

So let's assume the statement actually is about what programs can be expressed. Then it might still be false. In particular, heterogeneous collections can be expressed with parametric polymorphism, using existential types.

Formally, this fairly theoretic paper essentially shows that parametric polymorphism can encode subsumption. The inverse certainly is not true. So on a more theoretic level, the statement has it exactly backwards.

Good lectures teach you things. At any rate, I consider Meyer's conclusions to be interesting rather than conclusive--if for no other reason than the paper is 20 years old, and many advances in the theory have happened since then. Meyer's role as a language designer (and peddler of same) sometimes appears to taint his contributions as a theorist--that said, I consider OOSC still to be one of the seminal works on OOP--despite the drumbeat of Eiffel evangelism it contains.

On the other hand, there remains an interesting question: In my view, the defining characteristic of (typed) OO languages is potentially unrestricted subtyping and subsumption, however implemented. (By unrestricted; I refer to the fact that classes or what-have-you are typically not closed abstractions; another module or even another program may introduce a subclass which then can be substituted for the class, often in surprising ways.). Many authors in various contexts have expressed the opinion that this is a bad thing; Date and Darwen suggest limiting subtyping to strengthening of invariants; and the Cforall proposal seems to view a lack of subtyping as a good thing. Thoughts or papers which address this topic?

Many authors in various contexts have expressed the opinion that this is a bad thing; Date and Darwen suggest limiting subtyping to strengthening of invariants; and the Cforall proposal seems to view a lack of subtyping as a good thing. Thoughts or papers which address this topic?

It can be, as it can leak authority. For instance, if you subclass a type, then introduce new authority in the subclass, then provide the reference to some hostile code which expects the superclass, the hostile code can cast it to the concrete type, and extract more authority than you had intended to grant, and this type of code is very hard to audit. As Dean Tribble states in the above message:

Capability Design Rule #1: All distinctions in authority are represented by different capabilities. (Note that I'm rephrasing on the fly here to not confuse the people that still believe that objects are something you point to as opposed to the emergent phenomena of having pointed.

These sorts of unintended subtyping side-effects are pervasive, so in general, I'm starting to lean away from subtyping (at least OO forms of it).

module Univ = struct
 type t = { clear : unit -> unit;
            store : unit -> unit; }

 let embed () =
   let r = ref None in
   let inject a =
     { clear = (fun () -> r := None);
       store = (fun () -> r := Some a); }
   in
   let project u =
     u.store ();
     let res = !r in
     u.clear ();
     res
   in
     (inject,project)
end

let (inject_float,project_float) = Univ.embed ()
let (inject_int,project_int) = Univ.embed ()

let heterogenous_list = [ inject_float 4.; inject_int 5 ]
let just_floats = (* a list containing just the float 4. *)
   List.filter_map project_float heterogenous_list
let just_ints = (* a list containing just the int 5 *)
   List.filter_map project_int heterogenous_list

That is a universal type. Also note the MLton wiki page on UniversalType.