Quasi-static typing

We present a new approach to dynamic typing in a static framework. Our main innovation is the use of structural subtyping for dynamic types based on the idea that possible dynamic typing as a property should be inherited by objects of all types. Two properties of our system set it apart from existing systems which combine static and dynamic typing: all tagging and checking takes place via implicit coercions, and the semantics of dynamic typing is representation independent. The latter property leads to a significant increase in expressive power—for instance it allows us to define a general call-by-value fixpoint operator.The resulting system—which we call quasi-static typing—is a seamless merger of static and dynamic typing. The system divides programs into three categories: well-typed, ill-typed and ambivalent programs. Ill-typed programs contain expressions that are guaranteed to go wrong. Run-time checking is limited to doubtful function applications in ambivalent programs. Conceptually, quasi-static typing takes place in an unusual two-phase process—a first phase infers types and coercions and a second plausibility checking phase identifies ill-typed programs. The typing rules allow minimal typing judgements and plausibility checking can be characterized as simplification via a canonical set of rewrite rules. The two phase process can therefore be implemented with a one pass algorithm.