一句话：提出模块化的集合论类型表示，并重访子类型与 tallying 算法，评估优化与设计选择。
集合论类型支持并、交、补等丰富代数运算，并配有可判定的约束求解算法 tallying，适合为动态语言中兼具泛型与重载行为的函数建模，但其实现复杂阻碍了广泛应用。本文提出一种模块化的集合论类型表示，重新审视子类型与 tallying 算法，并将其与历史实现 CDuce 进行比较；同时评估若干优化和设计选择对性能的影响。结果展示了该表示与算法在实现可行性和性能上的权衡。
Set-theoretic types provide a rich type algebra that supports unrestricted unions, intersections, and negations, together with a decidable type constraint-solving algorithm known as tallying. These types are particularly well suited for typing dynamic languages, where functions often exhibit both generic and overloaded behavior. However, the complexity of their implementation has hindered their widespread adoption. In this paper, we introduce a modular representation for set-theoretic types and revisit the algorithms for subtyping and tallying. We compare our approach with the historical CDuce implementation and evaluate the performance impact of some optimizations and design choices.