Lambda the Ultimate

Much of the confusion here is because the paper deliberately conflates (dynamic) overriding with (static) overloading and treats both as parts of late binding semantics. I don't think that makes much sense. Admittedly, mixing both in the way e.g. C++ or Java do is not a good idea to start with.

Also, the paper's running example is too simplistic for languages with structural object types (like OCaml), where the three argument types collapse into one. For example, with a "real" example that adds methods along the T-M-B inheritance chain, the whole third column would be an error in Ocaml, because Down no longer is a subtype of Up (and the second column would contain errors, too).