Dynamic typing for distributed programming in polymorphic languages

While static typing is widely accepted as being necessary for secure program execution, dynamic typing is also viewed as being essential in some applications, particularly for distributed programming environments. Dynamics have been proposed as a language construct for dynamic typing, based on experience with languages such as CLU, Cedar/Mesa, and Modula-3. However proposals for incorporating dynamic typing into languages with parametric polymorphism have serious shortcomings. A new approach is presented to extending polymorphic lnanguages with dynamic typing. At the heart of the approach is the use of dynamic type dispatch, where polymorphic functions may analyze the structure of their type arguments. This approach solves several open problems with the traditional approach to adding dynamic typing to polymorphic languages. An explicity typed language XML dyn is presented; this language uses refinement kinds to ensure that dynamic type dispatch does not fail at run-time. Safe dynamics are a new form of dynamics that use refinement kinds to statically check the use of run-time dynamic typing. Run-time errors are isolated to a separate construct for performing run-time type checks