G. Richards, F. Zappa Nardelli, J. Vitek 1003
3 Background and Related Work
The divide between static and dynamic types has fascinated academics and practitioners for
years. Academics come determined to “cure the dynamic” as the absence of types is viewed
as a flaw. Practitioners, on the other hand, seek to supplement their testing practices with
machine-checked documentation and some ahead-of-time error checking. Dynamic languages
are appreciated by practitioners for their productivity, their smaller learning curve, and their
support of exploratory programming, as any grammatically correct dynamic program, even
a partial program or one with obvious errors, can be run. Decades of research were devoted
to attempts to add static types to dynamic languages. In the 1980’s, type inference and
soft typing were proposed for Smalltalk and Scheme [20, 3, 7]. Inference based approaches
turned out to be brittle as they required non-local analysis and were eventually abandoned.
Twenty years ago, while working at Animorphic on the virtual machine that would even-
tually become HotSpot, Bracha designed the first optional type system [6]. Subsequent work
fleshed out the design [4] and detailed the philosophy behind optional types [5]. An optional
type system is one that: (1) has no effect on the language’s runtime semantics, and (2)
does not mandate type annotations in the syntax. Strongtalk like Facebook’s Hack, Google’s
Dart, and Microsoft’s TypeScript was an industrial effort. In each case, a dynamic language
is equipped with a static type system that is flexible enough to support backwards compat-
ibility with untyped code. While optional types have benefits, they provide no guarantee of
absence of type errors nor information that could be relied upon by an optimizing compiler.
Another important line of research is due to Felleisen and his collaborators. After inves-
tigating soft typing approaches for Scheme, Findler and Felleisen turned their attention to
software contracts [9]. In [10], they proposed wrappers to enforce contracts for higher-order
functions; these wrappers, higher-order functions themselves, were in charge of validating
pre- and post-conditions and assigning blame in case of contract violations. Together with
Flatt, they turned higher-order contracts into semantics casts [11]. A semantics cast consists
of an argument (a value), a target type, and blame information. It evaluates to an object of
the target type that delegates all behavior to its argument, and produces meaningful error
messages in case the value fails to behave in a type appropriate manner. In 2006, Tobin-
Hochstadt and Felleisen proposed a type system for Typed Racket, a variant of Scheme that
used higher-order contracts to enforce types at module boundaries [21]. Typed Racket has
a robust implementation and is being used on large bodies of code [22]. The drawback of
this approach is that contracts impose a runtime overhead which can be substantial in some
programs.
In parallel with the development of Typed Racket, Siek and Taha defined gradual typing to
refer to languages where type annotations can be added incrementally to untyped code [18,
19]. Like in Typed Racket, wrappers are used to enforce types but instead of focusing on
module boundaries, any part of a program can be written in a mixture of typed and untyped
code. The type system uses two relations, a subtyping relation and a consistency relation
for assignment. Their work led to a flurry of research on issues such as bounding the space
requirements for wrappers and how to precisely account for blame. In an imperative language
their approach suffers from an obvious drawback: wrappers do not preserve object identity.
One can thus observe the same object through a wrapper and through a direct reference at
different types. Solutions are not appealing, either every property read must be checked or
fairly severe restrictions must be imposed on writes. In a Python implementation, called
Reticulated Python, both solutions cause slowdowns that are larger than 2x [23]. Another
drawback of gradual type systems is that they are not trace preserving. Consider:
E C O O P ’ 1 5