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.
翻译:许多面向对象的动态语言允许程序员从对象中抽取方法, 并将其作为函数处理。 这样可以允许灵活的编程模式, 但给类型系统带来挑战。 特别是, 简单处理方法提取方法需要方法在接收器类型中具有反向性, 使所有但不可能存在。 我们对此问题进行详细调查, 以及一个实施和评估的解决方案。 方法提取是许多动态类型和逐步类型语言的特征, 从 Python 和 PHP 到流程和 TypeScript 。 在这些语言中, 对象作为程序记录可以访问, 但也给类型系统带来挑战。 实施方法的提取程序将要求在接收器类型中出现反向反向反向反向反向, 程序处理程序程序程序程序可以被重新定位为可独立调用的函数。 程序员可以明确指定“ 此特性”, 当使用方法实施时, 以及一个执行方法的特性。 不幸的是, 我们所显示的多种渐进类型系统系统, 如 Typesc 和流动在方法的提取中是不准确的。 。 输入任何这样的系统的问题是 。 在输入任何系统里, 它所允许的灵活性必须用的方法在两个版本中, 格式中, 格式中, 格式中, 。 将使用的方法的变变的变的版本 。