|
Abstract : |
We describe a new method for polymorphic type inference for the dynamically typed language Scheme. The method infers both types and explicit run-time type operations (coercions) for a given program. It can be used to statically debug Scheme programs and to give a high-level translation to ML, in essence providing an "embedding " of Scheme into ML. Our method combines the following desirable properties: ffl It is liberal in that no legal Scheme programs are "rejected " outright by the type inferencer. ffl It is modular in that definitions can be analyzed independent of the context of their use. The inferred type scheme for a definition is safe for all contexts. This is accomplished by admitting type coercion parameters, resulting in a form of polymorphic qualified type system. ffl It infers both types and run-time type operations and places the latter opportunistically at any suitable program point, not only at data creation and destruction points. ffl It is very efficient. Its monomorphic fragment can be implemented in almost-linear time, and the full polymorphic calculus appears to be comparable with ML type inference in practice. ffl It is conservativeover simple and ML-polymorphic typing in that the type inferencer inserts no run-time type operations for ML-typable programs (it may add some coercion parameters, however). ffl It classifies subexpressions as either definitely type correct (requiring no run-time type checking), possibly type correct (requiring run-time type checking), or definitely type incorrect (definitely aborting). Our method is based on the formal type theoretic framework of dynamic typing, generalized to include polymorphic type coercions, recursive types, and polymorphic coercive types. In this regard it is most closely related to the soft, |
