# TR available: "Dynamic Types Have Existential Type"


Readers of this mailing list may be interested in the following technical
report, which has been submitted for publication.  Comments are welcome.

Dynamic Types Have Existential Type

Dominic Duggan
University of Waterloo Tech Report CS-94-36, Dec 1994.

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.  {\em 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.

Internet addresses where it may be retrieved:

ftp://theory.doc.ic.ac.uk/imported-papers/DugganD/dynamic-types.ps.gz