Dynamic typing for distributed programming in polymorphic languages

While static typing is widely accepted as being necessary for secure progra m execution, dynamic typing is also viewed as being essential in some appli cations, particularly for distributed programming environments. Dynamics ha ve been proposed as a language construct for dynamic typing, based on exper ience with languages such as CLU, Cedar/Mesa, and Modula-3. However proposa ls for incorporating dynamic typing into languages with parametric polymorp hism have serious shortcomings. A new approach is presented to extending po lymorphic languages with dynamic typing. At the heart of the approach is th e use of dynamic type dispatch, where polymorphic functions may analyze the structure of their type arguments. This approach solves several open probl ems with the traditional approach to adding dynamic typing to polymorphic l anguages. An explicitly typed language XMLdyn is presented; this language u ses 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 kind s to statically check the use of run-time dynamic typing. Run-time errors a re isolated to a separate construct for performing run-time type checks.