Red Echo

February 9, 2009

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.


  1. This was one of the concepts of Radian that I liked when we were in the beginning stages of designing the language. This neatly removes the silly requirement for a ton of numeric datatypes by basically having a “number” which you can constrain. Now the compiler can choose the best representation for you. It allows you to focus on the “what” and not the “how.” I really dig this! :-)

    Comment by Aaron Ballman — February 9, 2009 @ 11:30 am

  2. I’ve learned a lot about Radian just from the vague blog posts. Interesting project!

    I really like the concepts and the thought you’ve been putting into it. I wonder when it will begin its journey into a product- please let us know, even in hidden CTP form (I remember discovering some hidden C# v3 stuff a year before I was supposed to!). I’m always on board for at least one or two licenses of any language/product you are involved with. :)

    Comment by Travis — February 20, 2009 @ 10:13 pm