Soft typing

Abstract

Type systems are designed to prevent the improper use of program operations. They can be classified as either static or dynamic depending on when they detect type errors. Static type systems detect potential type errors at compile-time and prevent program execution. Dynamic type systems detect type errors at run-time and abort program execution. Static type systems have two important advantages over dynamic type systems. First, they help programmers detect a large class of program errors before execution. Second, they extract information that a compiler can exploit to produce more efficient code. The price paid for these advantages, however, is a loss of expressiveness, generality, and semantic simplicity. This paper presents a generalization of static and dynamic typing-called soft typing-that combines the best features of both approaches. The key idea underlying soft typing is that a static type checker need not reject programs that contain potential type errors. Instead, the type checker can insert explicit run-time checks around "suspect" arguments of primitive operations, converting dynamically typed programs into statically type-correct form. The inserted run-time checks identify program phrases that may be erroneous. For soft typing to be effective, the type system must avoid inserting unnecessary run-time checks. To accomplish this objective, we have developed an extension of the ML type system supporting union types and recursive types that assigns types to a wider class of programs than ML. We have also developed an algorithm for frugally inserting run-time checks in programs that do not type check.