一句话：提出 ZipML，以浮动字段和签名 zipper 消除 ML 模块的签名规避问题，并证明类型系统可靠。
ML 模块的签名规避问题会在签名匹配时破坏类型共享或迫使类型检查器引入额外声明。本文提出 ZipML：一种基于路径的类型系统，在签名中引入用户不可见但类型检查器可访问的浮动字段，并处理为签名上的 zipper。浮动字段可延迟问题求解，且因不存在于运行时，可随类型等价化简并在不可达时删除。作者给出保持类型共享的改写规则与实现算法；剩余浮动字段可在签名归属时消失，必要时才展示给用户以改善错误信息。ZipML 还支持 early/lazy strengthening 与定义惰性内联，避免签名重复。其正确性通过精化到 Mω、再翻译到 Fω 证明，设计可回填到 OCaml。
We present ZipML , a new path-based type system for a fully fledged ML-module language that avoids the signature avoidance problem. This is achieved by introducing floating fields , which act as additional fields of a signature, invisible to the user but still accessible to the typechecker. In practice, they are handled as zippers on signatures, and can be seen as a lightweight extension of existing signatures. Floating fields allow to delay the resolution of instances of the signature avoidance problem as long as possible or desired. Since they do not exist at runtime, they can be simplified along type equivalence, and dropped once they became unreachable. We give rewriting rules for the simplification of floating fields without loss of type-sharing and present an algorithm that implements them. Remaining floating fields may fully disappear at signature ascription, especially in the presence of toplevel interfaces. Residual unavoidable floating fields can be shown to the user as a last resort, improving the quality of error messages. Besides, ZipML implements early and lazy strengthening, as well as lazy inlining of definitions, preventing duplication of signatures inside the typechecker. The correctness of the type system is proved by elaboration into M ω , which has itself been proved sound by translation to F ω . ZipML has been designed to be an improvement over OCaml that could be retrofitted into the existing implementation.
@article{BlaudeauRR25,
title = {Avoiding Signature Avoidance in ML Modules with Zippers},
author = {Clément Blaudeau and Didier Rémy and Gabriel Radanne},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704902}
}