kirancodes.me
To Proof Maintenance & Beyond!

Dynamic Typing in a Statically-Typed Language

Martín Abadi, Luca Cardelli, Benjamin C. Pierce, Gordon D. Plotkin

Abstract

Statically-typed programming languages allow earlier error checking, better enforcement of disciplined programming styles, and generation of more efficient object code than languages where all type-consistency checks are performed at runtime. However, even in statically-type languages, there is often the need to deal with data whose type cannot be known 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.

Related papers