Gradual typing for first-class classes

Asumu Takikawa*, T. Stephen Strickland, Christos Dimoulas, Sam Tobin-Hochstadt, Matthias Felleisen

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

18 Scopus citations

Abstract

Dynamic type-checking and object-oriented programming often go hand-in-hand; scripting languages such as Python, Ruby, and JavaScript all embrace object-oriented (OO) programming. When scripts written in such languages grow and evolve into large programs, the lack of a static type discipline reduces maintainability. A programmer may thus wish to migrate parts of such scripts to a sister language with a static type system. Unfortunately, existing type systems neither support the flexible OO composition mechanisms found in scripting languages nor accommodate sound interoperation with untyped code. In this paper, we present the design of a gradual typing system that supports sound interaction between staticallyand dynamically-typed units of class-based code. The type system uses row polymorphismfor classes and thus supports mixin-based OO composition. To protect migration of mixins fromtyped to untyped components, the system employs a novel formof contracts that partially seal classes. The design comes with a theorem that guarantees the soundness of the type system even in the presence of untyped components.

Original languageEnglish (US)
Pages (from-to)793-810
Number of pages18
JournalACM SIGPLAN Notices
Volume47
Issue number10
DOIs
StatePublished - Oct 1 2012

Keywords

  • Blame theorem (proof technique)
  • Contracts
  • Design by contract
  • First-class classes
  • Gradual typing
  • Row polymorphism
  • Sealing

ASJC Scopus subject areas

  • Computer Science(all)

Fingerprint Dive into the research topics of 'Gradual typing for first-class classes'. Together they form a unique fingerprint.

Cite this