Key points are not available for this paper at this time.
Statically typed programming languages allow earlier error checking, better enforcement of diciplined programming styles, and the generation of more efficient object code than languages where all type consistency checks are performed at run time. However, even in statically typed languages, there is often the need to deal with datawhose type cannot be determined at compile time. To handle such situations safely, we propose to add a type Dynamic whose values are pairs of a value v and a type tag T where v has the type denoted by T . Instances of Dynamic are built with an explicit tagging construct and inspected with a type safe typecase construct. This paper explores the syntax, operational semantics, and denotational semantics of a simple language that includes the type Dynamic . We give examples of how dynamically typed values can be used in programming. Then we discuss an operational semantics for our language and obtain a soundness theorem. We present two formulations of the denotational semantics of this language and relate them to the operational semantics. Finally, we consider the implications of polymorphism and some implementation issues.
Abadi et al. (Mon,) studied this question.