深入解读 ty 集合论类型系统中的补类型 `~T`：从语义性质到源码实现

深入解读 ty 集合论类型系统中的补类型~T从语义性质到源码实现【免费下载链接】ruffAn extremely fast Python linter and code formatter, written in Rust.项目地址: https://gitcode.com/GitHub_Trending/ru/ruff~T是 ty 类型检查器位于本仓库crates/ty_python_semantic集合论类型系统中表示补集的一等类型构造它描述所有不属于T的值集合。本文以 type_compendium/not_t.md 这一官方 mdtest 文档为骨架逐一讲解~T与T的不相交性、T | ~T ≡ object、子类型/可赋值关系的反转、De Morgan 定律、渐变类型的否定等核心语义并对照crates/ty_python_semantic的集合论类型引擎源码与属性测试说明~T在底层是如何被表示和求值的。读完本文你将能读懂并亲手编写验证~T语义的 mdtest 断言理解补类型在类型收窄、穷尽性检查与泛型否定等场景中的工作原理。1. 什么是补类型~T在经典的面向对象类型系统中类型被理解为类的层次结构子类型关系由继承决定。而在 ty 采用的集合论set-theoretic类型模型中每个类型都被解释为一组值的集合。基于这种解释很自然地就可以引入集合的补运算~T是类型T的补集complement它描述的是所有不在T中的值。用集合论的记号写即~T { v | v ∉ T }。这也是为什么该文档所在目录名为type_compendium类型纲要——它与 intersection_types.md交集类型、联合类型等文档共同构成 ty 对集合论类型运算的完整说明体系。文档开头通过 TOML front-matter 指定了测试运行环境[environment] python-version 3.14这表明以下所有断言都基于 Python 3.14 的 typing 语义例如 PEP 604 的|联合语法与Any的渐变语义进行验证。2. 如何验证~T的性质mdtest 与类型断言工具not_t.md的正文完全由可执行的类型级断言构成。它使用了ty_extensions中提供的两个工具包ty_extensions.static_assert接受一个ConstraintSet约束集当该约束集被满足时静态断言通过ty_extensions._internal中的四个谓词is_disjoint_from不相交、is_equivalent_to等价、is_subtype_of子类型、is_assignable_to可赋值。它们的签名定义在 ty_extensions/_internal.pyi 中第 223265 行def is_equivalent_to(type_a: TypeForm[object], type_b: TypeForm[object]) - ConstraintSet: ... def is_subtype_of(ty: TypeForm[object], of: TypeForm[object]) - ConstraintSet: ... def is_assignable_to(ty: TypeForm[object], to: TypeForm[object]) - ConstraintSet: ... def is_disjoint_from(type_a: TypeForm[object], type_b: TypeForm[object]) - ConstraintSet: ...其中is_disjoint_from的 docstring 明确写道Two types are disjoint if they have no inhabitants in common两个类型不相交当且仅当它们没有任何共同的居民值。static_assert则定义在 ty_extensions/init.pyi 中。这些.pyi存根文件会被 ty 的类型检查器直接求值因此文档中的每一段 pyi 代码块实际上都是一次编译期单元测试——这正是 mdtestmarkdown 驱动的测试的机制README 式文档即测试测试即文档。掌握了这套断言语法我们就能像阅读数学定理证明一样逐条检验~T的每一条性质。3. 核心性质一~T与T不相交一个集合与其补集当然没有公共元素。文档用is_disjoint_from验证这一点并且强调不仅~T与T本身不相交与T的任意子类型S也不相交from ty_extensions import static_assert from ty_extensions._internal import is_disjoint_from class T: ... class S(T): ... static_assert(is_disjoint_from(~T, T)) static_assert(is_disjoint_from(~T, S))这里class S(T)声明S是T的子类因此S : TS的值集合是T值集合的子集自然也与~T不相交。从源码层面看这一性质被 ty 的否定即不相交逻辑所保证。在 types/property_tests.rs 中有一项当前被标记为 flaky 的属性测试与之对应// For any fully static type T, T should be disjoint from ~T. type_property_test!( negation_of_fully_static_types_is_disjoint, db, env, forall fully_static_types t. t.negate(db, env).is_disjoint_from(db, env, t) );即对任意全静态类型TT与其否定~T不相交是类型引擎内部通过negate()与is_disjoint_from()共同维护的不变量。4. 核心性质二T与~T的并集等价于object补集运算的一个直接推论是T和~T合在一起恰好覆盖全部值即它们的并集就是顶类型objectfrom ty_extensions import static_assert from ty_extensions._internal import is_equivalent_to class T: ... static_assert(is_equivalent_to(T | ~T, object))object在集合论类型模型中是全集任何类型的值集合都是它的子集T | ~T把T内外两侧全部取回正好回到全集。这条性质也是后续收窄到否定类型后再恢复类推理的理论基础——例如在if分支中先把变量收窄为~Telse分支再通过T | ~T ≡ object恢复原类型。5. 核心性质三~T反转子类型关系否定运算会反转子类型的偏序这与逻辑中否定反转方向完全一致若S : T则补集取反后方向反转得到~T : ~Sfrom ty_extensions import static_assert from ty_extensions._internal import is_subtype_of class T: ... class S(T): ... static_assert(is_subtype_of(S, T)) static_assert(is_subtype_of(~T, ~S))直觉上S ⊆ T那么T的补集~T全集去掉T必然是S的补集~S全集去掉S的子集——因为去掉的内容更少剩下的反而更多。ty 的类型引擎专门为这种结构化的否定子类型判断实现了快速路径。在 set_theoretic/builder.rs 中可以看到negation_is_subtype_of_cached这类带缓存的谓词调用并且属性测试文件里也保留了一条与该性质直接对应的属性测试// If S : T, then ~T : ~S. type_property_test!( negation_reverses_subtype_order, db, env, forall types s, t. s.is_subtype_of(db, env, t) t.negate(db, env).is_subtype_of(db, env, s.negate(db, env)) );该测试位于 property_tests.rs 的flaky模块中第 336339 行注释还说明它依赖 mdtest/type_properties/is_subtype_of.md 中对应的子类型简化测试通过后才能稳定——这体现了文档断言与属性测试互相印证的关系。6. 核心性质四~T反转可赋值关系可赋值关系is_assignable_to对应 typing 规范中的 assignable-to / consistent-subtyping 关系同样被补运算反转from ty_extensions import static_assert from ty_extensions._internal import is_assignable_to from typing import Any class T: ... class S(T): ... static_assert(is_assignable_to(S, T)) static_assert(is_assignable_to(~T, ~S))文档更进一步验证了在渐变类型参与下的反转仍然成立——即使类型被Any包裹static_assert(is_assignable_to(Any S, Any T)) static_assert(is_assignable_to(~(Any S), ~(Any T)))即若S可赋值给T那么Any S也可赋值给Any T交集保持可赋值性对两者取补后方向反转~(Any S)可赋值给~(Any T)依然成立。这说明反转律不仅对干净的类类型成立对包含渐变分量的交集类型也成立为实际代码中Any与否定类型混用提供了保证。7. 子类型与不相交性P、Q不相交蕴含P : ~Q补类型与不相交性之间有一条互为表里的等价关系若P与Q不相交则P必然是~Q的子类型反之亦然。文档用final类构造了两个必然不相交的类型from ty_extensions import static_assert from ty_extensions._internal import is_subtype_of, is_disjoint_from from typing import final final class P: ... final class Q: ... static_assert(is_disjoint_from(P, Q)) static_assert(is_subtype_of(P, ~Q)) static_assert(is_subtype_of(Q, ~P))final保证P、Q不存在其他子类从而它们各自的值集合就是类自身两个不同的 final 类必然不相交。由于Q的全部值都不在P中P的值自然全部落在~Q中即P : ~Q对称地Q : ~P。这条性质是穷尽性检查与收窄的核心工具当类型检查器需要证明某个分支不可达时本质上就是在论证该分支处的类型与当前已知类型不相交进而可以安全地收窄到对方的补类型。8. De Morgan 定律否定与并/交的互换集合论类型中的|并与交和逻辑中的∨、∧同构因此经典的 De Morgan 定律直接成立。文档先声明两个互不相关的类型P、Qfrom ty_extensions import static_assert from ty_extensions._internal import is_equivalent_to class P: ... class Q: ...定律一并集的否定等于否定的交集static_assert(is_equivalent_to(~(P | Q), ~P ~Q))定律二交集的否定等于否定的并集static_assert(is_equivalent_to(~(P Q), ~P | ~Q))这两条定律让类型检查器可以把不是P | Q重写为既不是P也不是Q~P ~Q从而把否定运算向下推到原子类型上逐项求值。由于 ty 的规范化表示中否定项被存储为交集的负元素见下一节De Morgan 定律正是这类重写得以成立的理论依据。9. 渐变类型的否定~Any等价于AnyAny是 Python typing 中的渐变类型gradual type它表示未知的值集合。文档指出对未知集合取补得到的仍然是一个未知集合因此两者等价from ty_extensions import static_assert from ty_extensions._internal import is_equivalent_to from typing import Any static_assert(is_equivalent_to(~Any, Any))这条性质对类型检查器的健全性至关重要与Any交互时类型检查器不能因为取了一次补就误以为自己获得了精确信息~Any ≡ Any保证了Any的渐变语义在补运算下保持封闭——~Any依然可以被赋值给任何类型、也可以从任何类型接收值不会引入虚假的错误。10. 源码实现~T如何被表示与求值理解了语义之后我们来看 ty 在 Rust 层面是如何落地~T的。与许多类型检查器例如基于模式匹配的穷举类型不同ty没有独立的否定类型节点而是把~T表示为以T为负元素的交集。这一点在 set_theoretic/builder.rs 文件头部的注释中写得很清楚No single-positive-element intersection types. Single-negative-element are OK, we dont have a standalone negation type so theres no other representation for this.不存在单一正元素的交集单一负元素是允许的因为我们没有独立的否定类型节点~T只能以此形式表示。在 set_theoretic.rs 中交集类型IntersectionType内部维护了两部分元素positive正元素集合negativeNegativeIntersectionElements即负元素被排除的项的紧凑集合。代码中还提供了若干与否定相关的判断与化简入口例如is_simple_negation第 1256 行附近判断一个交集是否恰好是正元素为空、仅有一个负元素的简单否定即~T的规范形态enum_complement第 796 行附近把Color ~Literal[Color.RED]这类枚举补集投影为紧凑的枚举补视图避免为排除字面量逐一展开。negate()求值路径生成~T则依赖IntersectionBuilder的add_negative接口把所有需要排除的类型塞进负元素槽位再经过规范化化简例如消去自相矛盾的T ~T分支、合并可互补的守卫对见builder.rs中Try to merge a complementary guarded pair into an unguarded core等逻辑得到最简形态。属性测试 property_tests.rs 对这一实现路径做了直接约束// Our optimized Type::negate() function should always produce the exact same type // as going the long way via the IntersectionBuilder. type_property_test!( all_negated_types_identical_to_intersection_with_single_negated_element, db, env, forall types t. t.negate(db, env) IntersectionBuilder::new(db, env).add_negative(t).build() );即Type::negate()的快速路径必须与通过IntersectionBuilder添加单个负元素的通用路径产生完全一致的类型同时double_negation_is_identity属性测试验证~(~T) ≡ T双重否定是恒等运算。这些测试与本文的 mdtest 文档从性质和实现两个方向共同锁定了~T的行为。另外值得注意的是文档第 3 节的~T与T不相交、第 5 节的反转子类型关系在 mdtest 的其他文档中也有呼应例如 intersection_types.md 中验证了object ~T等价于~T全集交集吸收律以及generics/pep695/functions.md、generics/legacy/functions.md中~T永远不可赋值给T的约束——这些都是理解补类型在泛型场景中行为的补充材料。11. 总结补类型~T在类型检查中的角色回顾not_t.md的完整论证链~T的语义可以浓缩为以下五条相互支撑的公理式性质性质断言用途不相交~T与T及T的子类型不相交分支收窄、不可达性证明互补性T \| ~T ≡ object类型恢复、穷尽性推理子类型反转S : T ⇒ ~T : ~S否定传播、方差推理可赋值反转S可赋给T⇒~T可赋给~S含Any混合场景一致性检查De Morgan~(P \| Q) ≡ ~P ~Q~(P Q) ≡ ~P \| ~Q否定下推化简渐变封闭~Any ≡ Any与Any交互时的健全性在 ty 的实现中~T被表示为单负元素交集并通过negate()/is_subtype_of/is_disjoint_from等核心 API 参与子类型与可赋值性判定property_tests.rs 中的属性测试与type_compendium目录下的 mdtest 文档互为印证。对于希望深入理解集合论类型系统或为 ty 贡献代码的读者建议按以下路径继续探索通读 type_compendium/not_t.md 及同目录其他类型纲要文档阅读 intersection_types.md 理解与负元素的配合对照 set_theoretic.rs 与 builder.rs 观察~T的表示与规范化运行 property_tests.rs 中的属性测试验证本文提到的各项性质在实现层面依然成立。补类型是 ty 区别于传统类层次类型检查器的重要能力之一它让类型检查器能够精确表达除X以外的一切从而在类型收窄、穷尽性检查与泛型否定场景中给出更精确、更符合程序员直觉的推断结果。【免费下载链接】ruffAn extremely fast Python linter and code formatter, written in Rust.项目地址: https://gitcode.com/GitHub_Trending/ru/ruff创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考