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: Chapter in Book/Report/Conference proceedingConference contribution

38 Scopus citations


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)
Title of host publicationSPLASH 2012
Subtitle of host publicationOOPSLA'12 - Proceedings of the 2012 ACM International Conference on Object Oriented Programming SystemsLanguages and Applications
Number of pages18
StatePublished - 2012
Event2012 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2012 - Tucson, AZ, United States
Duration: Oct 19 2012Oct 26 2012

Publication series

NameProceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA


Other2012 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2012
Country/TerritoryUnited States
CityTucson, AZ


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

ASJC Scopus subject areas

  • Software


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

Cite this