Scala is scary

This paper about DOT (= future Scala) has stuff that might be relevant to Wombat: http://arxiv.org/abs/1510.05216.

• "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.]

Units in Wombat

The way I hope to do units in Wombat is something like this:

There will be a type for length/distance. There will be some predefined values of that type such as metre. If you want 3.0 metres it is 3.0*metre. If you have a distance and you want to write it out as a number, divide by metre: myDist/metre. The same for angles: π*radian=180*degree. It gets a bit ugly for temperatures: zeroC+30.0*cDeg, and ditto date-time.

To be more exact. Assume the numbers we are working with are type Approx. Units will live in a type U. So metre above should really be U.metre, but there is nothing to stop you declaring `metre=U.metre, etc. The Approx number live in U as a degenerate set of units, so when you do myDist/metre you actually end up with type U, not type Approx. However Approx isA U. So, either immediately or at any later time, we can convert our result to Approx without failing.

[Update: This is just because units exist where we have a torsor (http://math.ucr.edu/home/baez/torsors.html): the difference or ratio is a number, but there is no default scale (multiplicative) or no certain starting point (additive), and the two variants seem to often come together. At any rate it is obvious that we want to generalize this and have type U be just a special case of a wider torsor type.]

[Update 2: Wouldn't it be better to have each sort of quantity (distance, mass, time, etc) be a different type? Then the type system could sort everything out, and detect mistakes at compile time, and some things become more convenient (distance1/distance2 is automatically just a number). But there are an infinite number of combinations (mass/(distance**3) is density) so it would be a complex variety of indexed types. This is very typical of the hard choices between static and dynamic typing. Wombat's standard library will try to hit the middle, while allowing others to do very static or very dynamic stuff. In this case a Distance type may not need any additional properties compared to type U restricted to distance. If that is the case then the advantages of having Distance as a separate type can be realised in a simple way using subset types, that is also pretty easy for the programmer to understand, and which let's them go back to U for one-off stuff without having to create new types all the time.]