Communications - February 2010

changed in a larger program, the type system will automatically point to all locations in the program that also need change. In a dynamically typed language it would be extremely difficult to make such changes in larger programs as it would be not known what other parts are affected by the change. On the other hand, some correct programs may be rejected by a static type system when it is not powerful enough to guarantee soundness.

In an effort to make static type systems more flexible, researchers have developed a number of extensions like interface polymorphism, a popular approach introduced by object-oriented languages like Simula, C++, Eiffel, Java, or C#. This method allows for inclusion between types, where types are seen as collections of values. So, an element of a subtype—say, a square—can be considered as an element of its supertype— say, a polygon—thus allowing the elements of different but related types to be used flexibly in different contexts.

Another form of polymorphism,
found in almost all programming lan-
guages, is ad hoc polymorphism (also
called overloading) where code be-
haves in different ways depending on
the type. This approach has found its
fullest expression in Haskell, thanks in
part to the efforts of Philip Wadler, pro-
fessor of theoretical computer science
at the University of Edinburgh. “When
we designed Haskell, it quickly became
clear that overloading was important
and that there was no good solution,”
says Wadler. “We needed overloading
for equality, comparison, arithmetic,
display, and input.”
The Haskell system has evolved con-
siderably over the years, thanks to the
contributions of a far-flung group of
contributors. “Once we’d come up with
the initial idea of type classes, it led to
a vast body of work, all sorts of clever
researchers coming up with neat exten-
sions to the system, or applying it do
things that we’d never thought it could
do,” says Wadler. Today, Haskell ranks
as the programming world’s premier
case study in ad hoc polymorphism.

The dream of unifying static and dynamic type systems has long fascinated researchers. Today, several computer scientists are probing the possibility of merging these approaches. Wadler is pursuing a promising line of research

the theory for
refinement types
has existed for
a long time, but
recent progress in
automatic theorem
proving makes
refinement types
suddenly practical.

called blame calculus that attempts to incorporate both static and dynamic typing, while Erik Meijer, a language architect at Microsoft Research, proposes to use “static typing when possible, dynamic typing when necessary.”

security type systems

In recent years, researchers have also been exploring type systems capable of capturing a greater range of programming errors such as the public exposure of private data. These emerging type systems are known as security type systems. Whereas a traditional type system enforces rules by assigning values to data types, a security type system could apply the same principle of semantic checking to determine the owner of a particular piece of information. Those annotations could then help ensure the integrity of data flowing through the system. Two promising security research projects include the AURA programming language, developed by Steve Zdancewic, associate professor of computer science at University of Pennsylvania, and Jif, a Java-based security-typed language developed by Andrew Myers, associate professor of computer science at Cornell University.

Another interesting application of
type checking involves hybridizing type
systems and theorem provers. “His-
torically, there have been two paral-
lel tracks in the software engineering
world: type systems and theorem prov-
ers. The type systems track has always
emphasized lightweight methods,”
says Benjamin C. Pierce, professor of
computer science at the University of
Pennsylvania, “but the formal methods
people aren’t interested in that. Today,
they’re starting to meet in the middle.”
Pierce points to refinement types,
which are types qualified by a logi-
cal constraint; an example is the type
of even numbers, that is, the type of
integers qualified by the is-an-even-
number constraint. While the theory
for refinement types has existed for
a long time, only recent progress in
automatic theorem proving makes re-
finement types suddenly practical. A
promising security project was recently
performed by Andrew D. Gordon, prin-
cipal researcher at Microsoft Research
Cambridge, and colleagues. They add-
ed a system of refinement types to the
F# programming language and were
able to verify security properties of F#
implementations of cryptographic pro-
tocols by type checking.