一句话：为同时支持函数式与命令式范式的动态语言提出基于集合论类型的类型系统与推断方法。
动态语言常混合函数式与命令式特性，已有基于集合论类型的重载与泛型函数类型推断难以直接处理可变状态和副作用。本文将相关工作扩展到不纯 λ 演算，针对 JavaScript、Python、Julia 等语言中的命令式特性设计类型系统，并提出用集合论类型表示参数化不透明数据类型，以精确建模可变数据结构，同时提升模块化、清晰性与可读性。作者还与现有方法进行比较，并在原型实现上通过一系列示例进行评估。
In this paper, we formalize a type system based on set-theoretic types for dynamic languages that support both functional and imperative programming paradigms. We adapt prior work in the typing of overloaded and generic functions to support an impure λ -calculus, focusing on imperative features commonly found in dynamic languages such as JavaScript, Python, and Julia. We introduce a general notion of parametric opaque data types using set-theoretic types, enabling precise modeling of mutable data structures while promoting modularity, clarity, and readability. Finally, we compare our approach to existing work and evaluate our prototype implementation on a range of examples.
@article{paperbot3783,
title = {Type Inference for Functional and Imperative Dynamic Languages},
author = {Mickaël Laurent and Jan Vitek},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA1},
year = {2026},
doi = {10.1145/3798220}
}