Typing is more complex than “dynamic” or “static”

This PDF slideshow introduces a concept the author calls “gradual typing” for Python. I’ve been pursuing a similar notion of typing in Radian. You can think of the notion of “type” as the information we have about a value. “Static type” is the information the compiler has about a value, and “dynamic type” is the information the running program has about the value.

From this perspective, one can see the ubiquitous ‘assert’ statement as a supplementary typing system, evaluated at run time. I frequently assert that various parameters are non-null, or that the objects in those parameters are related in some standard way; the C++ language may not include this information in its notion of a type system, but those attributes are very much part of my concept of the types I expect the method to receive. When you look at a type system in these broader terms, little islands of dynamic typing start to show up even in the most “static” languages like C++ and Java.

Wouldn’t it be nice if those ad-hoc assertions I place in my code by habit could be as much a part of the language, and have as much of an effect on the compiler’s knowledge about the values I am working with, as the built-in parameter and variable type annotations?

The Radian type system approaches something much like the linked presentation’s “gradual typing” from the opposite direction. It starts with a completely wide-open type system, where any value could have any type, then allows the programmer to limit the range of options by making assertions about values. Each assertion functions as a guard, or checkpoint; in order to continue, the given conditions must hold.

We then rely on dataflow analysis, constant propagation, and constant folding to resolve as many of these assertions as possible at compile time. The compiler can use the resulting knowledge about the content of each value to produce more efficient code specialized for that type. Each assertion condition can be resolved as either known true, in which case the assertion has been satisfied at compile time and can be omitted from the output, known false, in which case the compiler knows that the assertion cannot succeed and can report an error, or unknown, in which case the assertion will be compiled into the output and checked at run time.

Let’s make the compiler do all the tedious bookkeeping work! That’s what it’s there for. The result, I hope, will be a language which allows programs to start small, simple, and generic, then specialize over time for safety and efficiency – thus gaining the advantages of both “dynamic” and “static” typing.