[Prev][Next][Index][Thread]
Practical Soft Typing
I would like to announce the completion of my dissertation at Rice
University titled Practical Soft Typing. The thesis is available
by ftp from cs.rice.edu in public/languages/thesis-wright.ps.Z.
The abstract follows:
Soft typing is an approach to type checking for dynamically typed
languages. Like a static type checker, a soft type checker infers
syntactic types for identifiers and expressions. But rather than
reject programs containing untypable fragments, a soft type checker
inserts explicit run-time checks to ensure safe execution.
Soft typing was first introduced in an idealized form by Cartwright
and Fagan. This thesis investigates the issues involved in designing
a practical soft type system. A soft type system for a purely
functional, call-by-value language is developed by extending the
Hindley-Milner polymorphic type system with recursive types and
limited forms of union types. The extension adapts Remy's encoding of
record types with subtyping to union types. The encoding yields more
compact types and permits more efficient type inference than
Cartwright and Fagan's early technique. Correctness proofs are
developed by employing a new syntactic approach to type soundness. As
the type inference algorithm yields complex internal types that are
difficult for programmers to understand, a more familiar language of
presentation types is developed along with translations between
internal and presentation types. To address realistic programming
languages like Scheme, the soft type system is extended to incorporate
assignment, continuations, pattern matching, data definition, records,
modules, explicit type annotations, and macros. Imperative features
like assignment and continuations are typed by a new, simple method of
combining imperative features with Hindley-Milner polymorphism.
The thesis shows soft typing to be practical by illustrating a
prototype soft type system for Scheme. Type information determined by
the prototype is sufficiently precise to provide useful diagnostic aid
to programmers and to effectively minimize run-time checking. The
type checker typically eliminates 90\% of the run-time checks that are
necessary for safe execution with dynamic typing. This reduction in
run-time checking leads to significant speedup for some bench marks.
Through several examples, the thesis shows how prototypes, developed
using a purely semantic understanding of types as sets of values, can
be transformed into robust maintainable, and efficient programs by
rewriting them to accommodate better syntactic type assignment.
Andrew Wright