[Prev][Next][Index][Thread]

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:

        http://nuada.uwaterloo.ca/dduggan/papers.html#dynamic-types-paper

        ftp://nuada.uwaterloo.ca/pub/papers/dynamic-types.ps.gz

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

Please Note:

(1) The last of these may be faster for European colleagues, 
    since it is a UK ftp site.

(2) You need to use gunzip to uncompress the Postscript file.

-----
Spoken: Dominic Duggan        Internet: dduggan@uwaterloo.ca
Canada: Dept of Computer Science, University of Waterloo, 
        Waterloo, Ontario, Canada N2L 3G1
WWW:    http://nuada.uwaterloo.ca/dduggan.html