Dynamic Typing and Subtype Inference

Dynamic typing is a program analysis targeted at removing runtime tagging and untagging operations in dynamically typed languages. This paper shows that dynamic typing at least as powerful as Henglein's system [Hen92b] 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 Scheme) by removing runtime tests of type tags where they are provably unnecessary (so-called soft typing [CF91, WC94]). A remarkable, and to our knowledge unique, aspect of dynamic typing is that it not only permits the removal of dynamic type tag tests, but also allows the elimination of type tagging operations themselves..