Abstract Type systems are designed to prevent the improper SOFT TYPING

use of program operations. They can be classified as either static or dynamic depending on when they de-tect type errors. Static type systems detect potential type errors at compile-time and prevent program ex-ecution. 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 program-mers detect a large class of program errors before exe-cut ion. Second, the y extract information that a com-piler 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 un-derlying 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 p~imitive op-erations, converting dynamically typed programs into statically type-correct form. The inserted run-time checks identify program phrases that may be erro-neous. For soft typing to be effective, the type system must avoid inserting unnecessary run-time checks. To accomplish this objective, we have developed an exten-sion of the ML type system supporting union types and recursive types that assigns types to a wider class *The work of both authors was partially supported by NSF and DARPA. Permission to copy without fee ell or part of this material is granted provided that the copies are not made or distributed for direct commercial advantege, the ACM copyright notice and the title of the publication and its date appear, and notice is given that copying is by permission of th