- "extending subtyping to a lattice breaks at least one key metatheoretic property such as narrowing or subtyping transitivity". Apparently they solve the problem by distinguishing run-time values from those that exist at compile time but are never instantiated. This distinction is important in Wombat where infinite things exist at compile time.
- However the name DOT = "Dependent Object Types" makes me wonder. Objects are bags full of variables and variables preclude any sane type hierarchy because they can't behave covariantly or contravariantly with respect to any other type. I.e. if X isA Y then we can't create a rule that Assignable(X) isA Assignable(Y) because suppose we pass an Assignable(X) to a procedure that wants an Assignable(Y): that procedure might assign a Y to it that isn't an X. So I don't know how DOT can have sane semantics. I should add it to my list of "stuff I really should read", but I don't feel strong enough.
Jon Pretty gives another interesting talk: http://rapture.io/talks/slippery-surface/cadiz.html. I should try to understand how his ideas fit in with Wombat. His (and presumably Scala's) idea of intersection types is not the same as Wombat's.
The reason Wombat should (I expect) work without all the drama of more complex languages is the tough rule on the "isA" hierarchy: As you go up the hierarchy you always get less properties and the properties that are the same are (provably) compatible, and you have more data so that you can (provably) go back down the hierarchy with case statements and get back where you came from.
[Update: I should say something about what "compatible" means. One example is that addition works compatibly as you go from Int to Rational, even though one gives an Int result and the other a Rational result, the results are equal whether you promote the Int or demote the Rational. But it gets more complex when you get to things that don't support equality, particularly procedures. This shows up in the case of .asProc. We can use any type as if it was a procedure. For example "a string".length actually calls String.asProc("a string") with parameter .length. But .asProc is going to do less and less as we go up the hierarchy. So compatibility means that a higher .asProc might fail on a parameter, but if it succeeds it will return the same result (or compatible!!). A .asProc can take a parameter and pass it to the .asProc of all lower types (without having to know what they are) and combine the results. This is the equivalent of Abstract methods in other systems, but it has no problem with the situation where the value belongs to the intersection of multiple lower types.]