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.
Further Reading
Hindley, J.R.
Basic Simple Type Theory. Cambridge
University Press, new York, 2008.
Pierce, B.
Types and Programming Languages. MIT
Press, Cambridge, MA, 2002.
Flanagan, C.
hybrid type checking. SIGPLAN Notices 41,
1, Jan. 2006.
Cardelli, L.
Type systems. The Computer Science and
Engineering Handbook, Allen B. Tucker
(ed.). CRC Press, Boca Raton, FL, 1996.
Church, A.
A formulation of the simple theory of types.
Journal of Symbolic Logic 5, 2, 1940.
Alex Wright is a writer and information architect who
lives and works in brooklyn, Ny. Daan Leijen and Wolfram
Schulte of Microsoft research contributed to the
development of this article.