Dynamic Typing and Subtype Inference

Dynamic typing is a program analysis targeted at removing runtime tagging and untagging operations from programs written in dynamically typed languages. This paper compares dynamic typing with a subtyping system based on set constraints. The purpose is both to make precise the relationship between two superficially unrelated type systems and to illustrate how the advantages of dynamic typing and subtype inference can be combined. The central result is a theorem showing that a typing discipline at least as powerful as dynamic typing can be expressed using set constraints. 1 Introduction This paper presents a study of Henglein's dynamic typing discipline [Hen92a, Hen92b]. Dynamic typing extends conventional static types with a single new type Dynamic. Special functions called coercions inject values into and project values from type Dynamic. Currently, the main application of dynamic typing is the optimization of programs written in dynamically typed languages (such as Lisp and Schem..