Anzeige
Erschienen in:
2007 | OriginalPaper | Buchkapitel
Gradual Typing for Objects
verfasst von : Jeremy Siek, Walid Taha
Erschienen in: ECOOP 2007 – Object-Oriented Programming
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Static and dynamic type systems have well-known strengths and weaknesses. In previous work we developed a
gradual type system
for a functional calculus named
$\lambda^?_\to$
. Gradual typing provides the benefits of both static and dynamic checking in a single language by allowing the programmer to control whether a portion of the program is type checked at compile-time or run-time by adding or removing type annotations on variables. Several object-oriented scripting languages are preparing to add static checking. To support that work this paper develops
$\mathbf{Ob}^{?}_{<:}$
, a gradual type system for object-based languages, extending the
Ob
< :
calculus of Abadi and Cardelli. Our primary contribution is to show that gradual typing and subtyping are orthogonal and can be combined in a principled fashion. We also develop a small-step semantics, provide a machine-checked proof of type safety, and improve the space efficiency of higher-order casts.