Lambda the Ultimate

This doesn't sound like a subatantive change: if every class Foo implements an interface IFoo, then you can just change every variable of type Foo to be of type IFoo, except inside class Foo, of course (in Java/C# as well as C++, the unit of encapsulation is the class: you can change the private variables of other instances of your class).

The word "class", as it has been handed down by years and years of OOP, is in at least one way unfortunate; it differs quite a bit from its meaning in the relevant mathematics. In set theory, classes essentially are predicates on objects, which may or may not contain themselves (to avoid paradox). In most OO languages, classes are far more concrete than that, and only one thing in the broader universe of types.

Chris Date (in The Third Manifesto and other works) has a better term for the OO concept of class; "representation".

In many nominally-typed OO languages, classes give you three things:

1) They are the means of object creation--classes are those things which construct objects. Most OO languages allow multiple "constructors" to be contained within a single class; and once constructed, there is no difference between objects of the same class but created with different constructors. FP languages, which generally avoid the term "class"; do permit distinction between different branches of an algebraic sum; OTOH these often have different representations. GADTs (global abstract datatypes) are a useful extension here.

2) Classes are the repository of physical representation of objects. Objects have to ultimately live in memory somewhere and somehow; and have a well-defined (to the runtime at least; the details may be abstracted from the programmer) layout.

3) They are the types themselves. In an OO language, depending on context, this is a source of much perniciousness. A class may represent all the objects created with a particular layout (which would excluded public subclasses); OR it can mean the union of all objects belonging to the class or its subclasses. One reason that "base classes should be astract" is popular advice in OO circles, and that Java interfaces and similar are widely seen as good things, is that both of these techniques effectively make one of the two branches of this ambiguity the empty set. If a class or interface doesn't have any members of its own; then its only purpose in life is to represent the universe of its subtypes.

The moral of the story, then, is--and you are partially along the path to wisdom :)--decouple representation from the notion of type. Of course, "objects with representation X" is just as legit a type as "objects which implement interface Y" (for Java-style interfacing) or "objects which contain method M" (for structural/duck typing). There is no reason to disallow variables from having a concrete (class/representation) type; the problem with C/C++/Java is there is no way to say "an object of type X only; excluding subtypes".

There are, of course, types which are smaller than classes; "predicate types" or "subranges" are one example. There are many other interesting and useful ways to construct types that aren't generally found in the OO universe. Sum types are a highly useful one.

Not sure it meets your criteria, but Modula3 differentiates between Interfaces (type definition) and Implementation (modules).

(And Sather separated the concept of type inheritance from implementation inheritance).

OCaml and Sather both do what you want. Of these, OCaml is much more interesting, though: object types are structural interfaces that can be fully inferred. Classes are just stylised ways to create objects (and convenient type abbreviations).

As I recall, Sather is the language build around that concept.

OCaml, as mentioned above, is similar at first glance (though for different reasons altogether - what it does could be called "static duck typing").

It's late, and I'm not sure that I am fully processing the question, but the following note about how objects are to be implemented in BitC may be relevant.

Basically, our objects look a lot like Java interfaces, and carry no information in their type about representation at all. The only reason we have the construct in the language is for support of existential typing. Re-use in the style of inheritance is handled through type classes, which are rather different from traditional OO classes.

This paper proposes a separation of subclassing and subtyping, such that one can create subtypes of a class (viewed as a type) without inheriting its implementation. This sounds like what you want to achieve.