Dynamic Typing in Polymorphic Languages

There are situations in programmingwhere some dynamic typing is needed, even in the presence of advanced static type systems. We investigate the interplay of dynamic types with other advanced type constructions, discussing their integration into languages with explicit polymorphism (in the style of system F ), implicit polymorphism (in the style of ML), abstract data types, and subtyping. Contents 1 Introduction 1 2 Review 2 3 Explicit Polymorphism 4 3.1 Higher-order pattern variables : : : : : : : : : : : : : : : : : : : : 4 3.2 Syntax : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 6 3.3 Tag closure : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 7 3.4 Definiteness and matching : : : : : : : : : : : : : : : : : : : : : : 8 4 Implicit Polymorphism 10 4.1 Implicit tagging : : : : : : : : : : : : : : : : : : : : : : : : : : : : 10 4.2 Tag instantiation and tuple variables : : : : : : : : : : : : : : : : 11 4.3 A language : : : : : : : : : : : : : : : ..