Cycles without pollution: A gradual typing poem

It is fairly intuitive that adding dynamic typing to a statically typed language can add some convenience to a developer, at the price of weakening the guarantees of the type system. Surprisingly, the reverse is also true. This paper presents a programming poem á la Dan Friedman illustrating that temporarily circumventing the type system via a gradual typing cast can actually strengthen the guarantees of the type system overall. The paper first presents a challenge to write a small but interesting program. It proceeds by exploring how it could be written in Haskell and in SML (showing and discussing runnable code). It then gives the Typed Scheme version in a slower, more tutorial style, since the reader is assumed to be more familiar with Haskell and SML than Typed Scheme. Along the way, the paper shows how the Typed Scheme version overcomes weaknesses in the earlier versions. The key insight is that gradual typing enables us to view a data structure with two different types, one during the creation and one during use. The type during creation allows more operations that are needed to build an element of the data structure, and the type during use exposes more invariants of the data structure that can then be used to guarantee properties of the clients (termination, in this case).