This University of Waterloo Tech Report (CS-94-36, Dec 1994) has been submitted for publication.
Abstract: While static typing is widely accepted as being necessary for secure program execution, dynamic typing is also viewed as being essential in some applications. Dynamics have been proposed as a way of introducing dynamic typing into statically typed languages, with particular application to programming in distributed environments. However proposals for incorporating dynamics into ML-like polymorphic languages have serious shortcomings. A new approach is presented to extending ML-like languages with dynamic typing, with similar applications to dynamics. The approach is a refined notion of dynamics, with new introduction and elimination rules which overcome the problems with dynamics for polymorphic languages. This approach is extended to a model of objects and typing for ML-like languages. The resulting type system reflects functionality which is found in the Modula-3 monomorphic object-oriented distributed programming language. The semantics for this are expressed in a calculus with predicative effective polymorphism and impredicative existential types. A structural operational semantics is presented and used to verify a form of semantic soundness for the calculus, isolating all run-time type errors to well-formed run-time type checks due to narrowing. Combined with related work on providing objects with polymorphic methods, this demonstrates for the first time how effective polymorphism and first-class polymorphism may safely co-exist in the same language.
The report is available on the WWW and by anonymous ftp from a Canadian site or from a European site .