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`…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
