More rambling on Types

What is the difference between static and dynamic typing? In real life they blend into each other, which is why we see the big interest in gradual typing.

At one extreme we have the idea that "the Type is everything known about the value of an expression". In this space we have static typing if the compiler knows as much about the value of the expression as the programmer. Now the programmer is likely to know quite a lot about every expression in the program, and how it relates to other expressions. The compiler will certainly generate better code and give better error messages if it knows all that stuff too. But it is a bit unrealistic. In Wombat the programmer can put in as many or as few failure-inducing tests as he likes, and these potentially give information to the compiler to use.

At the other extreme we have the view that "a Type is constructed (and deconstructed) using a set of operations provided by the programming language". In such a static typing environment then the Type (in that sense) is always known at compile time. I would add that statically typed software is then expected to be written in such a way that it assumes no additional knowledge about values beyond the Type. It is certainly part of the plan that Wombat's general purpose libraries can be written this way, but I don't think it is practical to write many actual specific programs in that style.

In this latter view of the world the thing that makes a program dynamically typed is that the same expression can have different Types during different passes through the same section of code. This certainly seems undesirable. However this is something that always happens in languages with subtyping like OO languages and Wombat. A variable myMammal might be a Dog sometimes and a Cat at others, but it is always a Mammal. In Wombat this is taken to extremes so that every value belongs to a whole lattice (http://en.wikipedia.org/wiki/Lattice_%28order%29) of types, with Any at the top and the subset type that contains only itself at the bottom.