Lambda the Ultimate

In the lambda-cube the three axes represent static relationships that are formalized through a type system, your first example seem more dynamic and not that easily integrable in the Cube systems:

- sub-typing in Java, C++ and C#: if you refer to dynamic, late-bound overloading then I guess we could say it's a term-depending-on-type mixed with a term-depending-on-term: the behavior depends on the overloaded method definition which is chosen depending on the runtime type.

- Typeclasses, templates and generics are all instances of static types-depending-on-types, with resolution of classes and instantiation of templates and generics happening at type-checking. However, typeclasses and templates give you terms-depending-on-types because of specializations while generics give you by definition the same behavior for any type (or so I hope, at least parametric polymorphism does).

Isn't sub-typing, in the manner of Java, C++ and C#, an example of plain terms-depending-on-types?

No, subtyping is an entirely different dimension. The canonical example of "terms-depending-on-types" would be parametric polymorphism, as e.g. found in ML or as exemplified by generic methods in some OO languages.

Are prototype-based languages, such as Javascript, plain terms-depending-on-terms?

Javascript is untyped, so it's outside the classification of the lambda cube. A better example would be, say, Pascal. Prototypes don't have any relevance to this.

Are multi-parameter typeclasses, C++ templates and "generics" examples of types-depending-on-types? Are associated types (for example, the iterator for a certain collection) "higher-order" or are they essentially the same thing?

The primary examples of type constructors ("types-depending-on-types") are parameterised type definitions as found in ML or Haskell.

Type classes again are a different dimension, sometimes called "qualified types".

C++ templates are essentially untyped macros, but ignoring that fact (and a couple of others) you could view class templates as type constructors ("types-depending-on-types") and function templates as polymorphic functions ("terms-depending-on-types"). They can even be higher-order to a limited extent, by using "template template arguments".

"Generics" a la Java or C# provide a somewhat more principled implementation of similar concepts. They are not higher-order. Scala has fully higher-order generics and member types.

Associated types as in C++ or Haskell are slightly different, and are rather interpreted as type-indexed families of types - which means that their definitions are not uniform for different arguments. In fact, the same could already be said about C++ templates, since template specialisation might render them non-uniform - but it is largely moot trying to give a proper type-theoretic categorisation to C++.

As for dependent types ("types-depending-on-terms"), they hardly show up in today's mainstream languages. They can be found in the languages of provers like Coq, Twelf, or Agda. If you wanted, you could view C-style array types with their bounds as a very simple instance of a dependent type.

[Oops, wrong Reply button. Meant as reply to this post.]

How do we understand sub-typing in the context of the lambda calculus?

Well, subtyping is well-understood in the LC as just that, subtyping. Pierce's "Types and Programming Languages" discusses it in great detail.

But from your original question and Matthieu's reply I gather that by subtyping you actually mean late binding. However, this has nothing really to do with subtyping - not even with typing. It exists in untyped languages, too, e.g. prototype-based OOPLs. Late binding is just an ad-hoc form of higher-order argument passing. That some languages tie it to classes and subclassing (which isn't the same as subtyping, btw) is just an artefact of these languages.

Is this why sub-typing (to paraphrase Wadler) "is evil"?

Subtyping is often deemed evil because the meta-theory of a type system including it becomes much more complicated. Worse, it tends to destroy certain useful meta-theoretical properties. As a result, complete type inference is practically intractable for the simplest systems already, and in more expressive ones even decidability of mere type checking can quickly go overboard. From a practical perspective, types become less accurate and implementation more expensive, because subtyping polymorphism applies everywhere implicitly.

[Oh my, used the wrong comment field again. I should stay in bed where I belong.]

I agree that subtyping mainly adds convenience. You can almost always translate it away using explicit coercions or injections. Still, I don't understand what you mean. What is "true" subtyping? And what "dependencies" are you referring to?