[L2] ================================================ AMAST Links 02 02

                  Dynamic Types Have Existential Type
                           by Dominic Duggan

  This University of Waterloo Tech Report (CS-94-36, Dec 1994) has
been submitted for publication.

  *Abstract:* While static typing is widely accepted as being necessary
for secure program execution, dynamic typing is also viewed as being 
essential in some applications.  _Dynamics_ have been proposed as 
a way of introducing dynamic typing into statically typed languages, 
with particular application to programming in distributed environments.
However proposals for incorporating dynamics into ML-like polymorphic 
languages have serious shortcomings.  A new approach is presented to 
extending ML-like languages with dynamic typing, with similar 
applications to dynamics.  The approach is a refined notion of 
dynamics, with new introduction and elimination rules which overcome 
the problems with dynamics for polymorphic languages.  This approach is
extended to a model of objects and typing for ML-like languages.  The 
resulting type system reflects functionality which is found in the 
Modula-3 monomorphic object-oriented distributed programming language. 
The semantics for this are expressed in a calculus with predicative 
effective polymorphism and impredicative existential types.  A 
structural operational semantics is presented and used to verify a form
of semantic soundness for the calculus, isolating all run-time type 
errors to well-formed run-time type checks due to narrowing.  Combined 
with related work on providing objects with polymorphic methods, this 
demonstrates for the first time how effective polymorphism and 
first-class polymorphism may safely co-exist in the same language.

  The report is available on the WWW at
URL: http://nuada.uwaterloo.ca/dduggan/papers.html#dynamic-types-paper
and by anonymous ftp from a _Canadian site_ at
URL: ftp://nuada.uwaterloo.ca/pub/papers/dynamic-types.ps.gz
or from a _European site_ at URL:
ftp://theory.doc.ic.ac.uk/imported-papers/DugganD/dynamic-types.ps.gz