Type Checking Extracted Methods

TL;DR

This paper investigates the challenges of type checking for method extraction in object-oriented dynamic languages, proposing a sound solution combining existential types and occurrence typing, formalized and implemented in Typed Racket.

Contribution

It introduces a novel type system extension that ensures soundness for method extraction, integrating existential types and occurrence typing in Typed Racket.

Findings

Existing type systems like TypeScript and Flow are unsound with method extraction.

The proposed approach is formalized and proven sound.

Implementation in Typed Racket is compatible with existing packages.

Abstract

Many object-oriented dynamic languages allow programmers to _extract methods_ from objects and treat them as functions. This allows for flexible programming patterns, but presents challenges for type systems. In particular, a simple treatment of method extraction would require methods to be contravariant in the receiver type, making overriding all-but-impossible. We present a detailed investigation of this problem, as well as an implemented and evaluated solution. Method extraction is a feature of many dynamically-typed and gradually-typed languages, ranging from Python and PHP to Flow and TypeScript. In these languages, the underlying representation of objects as records of procedures can be accessed, and the procedures that implement methods can be reified as functions that can be called independently. In many of these languages, the programmer can then explicitly specify the `this` value to be used when the method implementation is called. Unfortunately, as we show, existing gradual type systems such as TypeScript and Flow are unsound in the presence of method extraction. The problem for typing any such system is that the flexibility it allows must be tamed by requiring a connection between the object the method was extracted from, and the function value that is later called. In Racket, where a method extraction-like facility, dubbed "structure type properties", is fundamental to classes, generic methods, and other APIs, these same challenges arise, and must be solved to support this feature in Typed Racket. We show how to combine two existing type system features -- existential types and occurrence typing -- to produce a sound approach to typing method extraction. We formalize our design, extending an existing formal model of the Typed Racket type system, and prove that our extension is sound. Our design is also implemented in the released version of Racket, and is compatible with all existing Typed Racket packages, many of which already used a previous version of this feature.