PyCon US 2026 类型峰会回顾

# PyCon US 2026 类型峰会回顾 来源：https://bernat.tech/posts/pycon-us-2026-typing-summit-recap/ PyCon US 2026 类型峰会 (https://us.pycon.org/2026/events/typing-summit/) 于 2026 年 5 月 14 日星期四下午 1 点至 5 点在长滩会议中心 201A 室举行，比主会议早一天。共有八场演讲加上一场类型委员会问答，单轨道。这篇回顾是为那些无法亲临现场的人准备的。 TLDR： - Guido van Rossum 认为，PEP 484 (https://peps.python.org/pep-0484/) 的“无新语法”规则在实践中已被打破，该领域应根据 2025 年 Python 类型调查 (https://engineering.fb.com/2025/12/22/developer-tools/python-typing-survey-2025-code-quality-flexibility-typing-adoption/) 的结果，将用户痛苦置于强大功能之上。 - Jelle Zijlstra 提议在类型规范中添加交类型和受限否定类型，并引入居住性检查作为新的核心规则。 - Michael Sullivan 提出了 PEP 827 (https://peps.python.org/pep-0827/) (Vercel)，用于类型操作，其模型基于 TypeScript 的条件类型和映射类型。 - Douglas Creager 展示了 `ty` 如何使用三元决策图内部表示泛型调用约束，以及第三种求解器策略，该策略修复了一个 9 行的 `partial(choose, None)` 示例——所有生产检查器目前都会弄错这个例子。 - Conner Nilsen 展示了一项关于 Pyrefly 与 AI 编码代理的实验：类型检查使 Meta 内部类型良好的代码的成功率从 79.6% 提高到 83.9%，步骤减少 21%；但在类型检查较轻的 SWE-bench Verified 上无明显帮助。 - Avik Chaudhuri 演示了 Pyrefly 中的张量形状类型，但在实践中受到 PEP 695 (https://peps.python.org/pep-0695/) 对类型参数急切求值的阻碍。 - Jia Chen 提出了一个用 Lean 4 形式化的方案（Featherweight Python），包含机械化的可靠性和可判定性证明；AI 辅助工具将过去需要数年的工作缩短到了数周。 - 类型委员会小组讨论（Carl Meyer、Jelle Zijlstra、Rebecca Chen 在场）开放提问，涉及治理、错误码一致性、元编程和规范方向。 ## 使用 AI 代理和 Pyrefly 类型错误进行实验——Conner Nilsen 指向标题的链接 (https://bernat.tech/posts/pycon-us-2026-typing-summit-recap/#experiments-with-ai-agents-and-pyrefly-type-errors--conner-nilsen) Conner Nilsen 关于以更高频率向代理提供反馈的发现幻灯片 Conner（Meta，Pyrefly (https://pyrefly.org/) 团队）提出了两个问题：（1）给 AI 编码代理一个类型检查器是否有助于它完成任务；（2）它是否能防止代理在修复新错误时重新引入旧错误？他的团队在两个基准上进行了有无类型检查器反馈的测试，并跟踪了三个指标：成功率、完成步骤数和实际耗时。 问题 1 的答案取决于代码覆盖范围。 - **类型良好的代码**（一个内部 Meta 基准）：成功率从 **79.6% 提升到 83.9%**，**步骤减少 21%**，**实际运行时间缩短 14%**。类型检查器在代理进行探索之前就捕获了问题。 - **类型化程度较低的代码**（SWE-bench Verified (https://www.swebench.com/)，涉及 Django、SymPy、Matplotlib 等库）：没有显著改善。代理将步骤浪费在任务附近代码的类型错误上，修复与所分配错误无关的导入不匹配和缺失属性。 问题 2 的答案是肯定的：有了类型检查器参与，代理在修复新错误时不会再重新引入之前修复的错误。 关于交付机制的两项发现： 1. **模型不会仅仅因为你提到工具就使用它们。**告诉代理“你可以运行类型检查器”是不够的。团队将 Pyrefly 调用包装在一个轻量级的思考-行动-观察循环中，该循环在每次编辑后运行类型检查器并注入结果。有了这个包装器，两个模型都会处理错误。没有它，它们就不会处理。 2. **将错误作为新的对话轮次呈现，而不是作为编辑工具的输出。**在前一个工具响应中返回的错误会被视为噪音。同样的错误以新轮次的形式发布时，则会被处理。 模型敏感性存在差异。Claude Sonnet 4.5 (https://www.anthropic.com/news/claude-sonnet-4-5) 会追逐类型检查器发出的每一个错误，这在代码清晰时很有帮助，但在代码嘈杂时则有害：模型会在返回任务之前修复不相关的干扰项。GPT-5 codex 则保持目标导向，除非包装器强制将错误引入对话，否则会忽略它们。 未解决问题幻灯片指出了后续方向：SWE-bench Verified 不是这个问题适合的基准测试，因为任务本身很少需要类型推理。一个基于类型化程度较高的项目的基准测试才能告诉你类型检查对代理是起关键作用还是在边缘有所帮助。 ## `ty` 对约束集的实现——Douglas Creager 指向标题的链接 (https://bernat.tech/posts/pycon-us-2026-typing-summit-recap/#the-ty-implementation-of-constraint-sets--douglas-creager) Douglas Creager 在讲台上展示“此表达式何时有效？”幻灯片，其中包含 `def identity T x T to T` 和 `result int = identity 2` Doug（Astral，其标题幻灯片上标注为“OpenAI 联合项目”）讲解了 `ty` (https://docs.astral.sh/ty/) 如何表示泛型函数调用的状态。他借助一个 9 行的程序进行说明，该程序运行良好，但每个生产型检查器都会拒绝，并通过 multiplay (https://github.com/astral-sh/multiplay)（Astral 的一款工具，可并排运行多个类型检查器检查 Python 代码段）进行了现场演示。幻灯片：dcreager/presentations (https://github.com/dcreager/presentations/raw/typing-summit/2026-05-typing-summit/dcreager-typing-summit-2026-slides.pdf) ```python def choose[A](a1: A, a2: A) -> A: return random.choice([a1, a2]) def partial[X, Y, Z](fn: Callable[[X, Y], Z], x: X) -> Callable[[Y], Z]: ... p = partial(choose, None) p(2) # 类型检查器：错误。参数 2 不是 None。 p("hello") # 同样错误。 ``` 直接调用 `choose(None, 2)` 类型检查没问题：`A` 求解为 `None | Literal[2]`（或 `None | int`，取决于检查器）。但通过 `partial` 路由就不行。Doug 用 `mypy`、`pyright`、`pyre`、Pyrefly 和 `ty` 运行了这个程序，每个都给出了错误答案。 他的重新表述：与其问“这个表达式有效吗？”，不如问 **“这个表达式何时有效？”** 答案是一个关于类型变量的布尔谓词，等价于一组有效赋值。每个类型检查步骤都会向集合添加一个子类型约束： - 对于直接调用：`{Literal[2] ≤ A, None ≤ A}`。 - 对于部分应用：`{None ≤ X, X ≤ A, Y ≤ A, A ≤ Z}`。 Doug 向观众讲解了针对 `partial(choose, None); p(2)` 示例的三种求解器策略。前两种是目前生产检查器所做的，会在不同方向上产生错误答案；第三种则重现了直接调用的答案。 | 策略 | 作用 | `p` 的推断类型 | `p(2)` 的结果 | |------|------|----------------|----------------| | 1 | 根据可见约束急切求解 `Y` 和 `Z` | `Callable[[None], None]` | `invalid-argument-type`：`2` 不是 `None` | | 2 | 将 `Y` 和 `Z` 映射到 `A`，从代换中删除 `A` | `Callable[[A], A]` | 接受，但 `A` 的解丢失了 `None`：仅有 `Literal[2]` / `int` | | 3 | 将整个约束集作为潜在的泛型向前传递 | `Callable[[Y], Z]` 并附加 `Y ≤ Z ∧ None ≤ Z` | 与直接调用答案相同：`Y = Z = None | Literal[2]` | Astral 正在将 `ty` 迁移到第三种策略；该工作尚未公开发布。 Doug 讲解了 `ty` 如何在内部表示约束集：**三元二叉决策图**，即 BDD 扩展出第三条“不确定”边，并与 Horn 子句风格的派生事实引擎组合以实现传递性。他将 BDD 变体归功于 Guillaume Duboc 的 *Typing Dynamic Languages with Set-Theoretic Types: The Case of Elixir* (https://gldubc.github.io/)，该论文于 2026 年 1 月 19 日在巴黎 IRIF 答辩通过，更广泛的背景见 Elixir 集合论类型项目 (https://elixir-lang.org/blog/2023/06/22/type-system-updates-research-dev/)。关于子类型推断和将约束具体化为类型，他引用了 Stephen Dolan 的 *Algebraic Subtyping* (https://www.cs.tufts.edu/~nr/cs257/archive/stephen-dolan/thesis.pdf) (剑桥，2017)。 Doug 提出了两个未解决的问题： 1. 类型规范是否应该增加“约束可调用类型”，还是这仍然是 `ty` 的实现细节？ 2. 如果约束被具体化为类型，如何向用户报告矛盾？每个约束都需要一个指向引入该约束的源码范围的回指指针，否则错误消息就会退化为“某处出错了”。 ## 在 Lean 中形式化 Python 类型化的部分内容——Jia Chen 指向标题的链接 (https://bernat.tech/posts/pycon-us-2026-typing-summit-recap/#formalizing-parts-of-python-typing-in-lean--jia-chen) Jia Chen 的静态定理幻灯片：如果类型检查器接受一个程序，那么运行它不会遇到运行时类型错误 Jia（Meta，Pyrefly 团队）展示了一个副项目：用 Lean 4 (https://lean-lang.org/) 编写的 Python 子集的机械化形式化，其定理由 Lean 的内核验证。他称之为 Featherweight Python，沿袭了 Featherweight Java (https://www.cis.upenn.edu/~bcpierce/papers/fj-toplas.pdf) 的命名传统。该项目是非正式的，尚未发布。Jia 用它来回答那些类型规范未说明且性能测试结论不确定的设计问题，然后再决定在 Pyrefly 中实现什么。 该工件包含五个 Lean 模块：源语言、解释器、类型检查器、定理陈述和证明。Lean 编译器要么接受整个包（定义良好，所有证明有效），要么拒绝它。该项目总共约 39,000 行 Lean 代码，其中渐进类型层的大小大约是静态层的两倍。静态层花了他一周时间；渐进层大约花了一个月。 两个静态侧定理支撑了这场演讲： - **可靠性。** 如果类型检查器接受一个程序，那么运行它不会遇到运行时类型错误。 - **可判定性。** 类型系统对应一个可终止的算法。 将这些写下来迫使 Jia 将非正式讨论中隐含的假设表面化：类层次遵循 Liskov 替换原则 (https://en.wikipedia.org/wiki/Liskov_substitution_principle)；MRO 有效且无环；世界是开放的，因此类型检查器无法枚举可能存在的每个类。 开放世界的选择约束了类型系统。否定类型作为集合补集（所有不是 `T` 的东西）需要一个固定的宇宙来减，而开放世界无法提供这一点。Jia 将否定限制为单个类，其缺失可以在运行时通过 `isinstance` 观察到。杰勒的交类型演讲后来在下午也遇到了同样的约束。 对于渐进层，Jia 重新表述了定理。有了 `Any` 的存在，可靠性直接失败；你无法证明“不会出错”。可挽救的属性是：每个失败都能追溯到某个 `Any` 边界。证明的方法是重写程序，在每个 `Any` 到静态的转换处插入运行时检查，然后证明任何检查失败都指向引入了 `Any` 的注解。没有 `Any` 的代码保持受保护；选择退出静态侧的部分是唯一可能失败的部分。 结尾的元要点落在了工具上。Jia 五年前曾试图启动这样一个项目，但因手工编写形式化证明太慢而放弃了。借助最近的 AI 辅助，计算方式发生了变化。架构工作仍由人类完成：选择语言、决定证明哪些定理、识别失败的证明尝试是否隐藏了真正的设计问题。机械化的证明编写则交给 AI。Jia 估计，渐进层花了他几周的时间，而不是几年。 ## 在 Pyrefly 中探索张量形状类型——Avik Chaudhuri 指向标题的链接 (https://bernat.tech/posts/pycon-us-2026-typing-summit-recap/#exploration-of-tensor-shape-types-in-pyrefly--avik-chaudhuri) Avik Chaudhuri 的“为什么”幻灯片，展示了 nanoGPT 风格的 PyTorch 代码，其中包含手写的形状注释元组 Avik（Meta）以 Andrej Karpathy 的 nanoGPT (https://github.com/karpathy/nanoGPT/blob/master/model.py) 的截图开场，这是一种 PyTorch 代码，其中每个张量操作都带有一个手写的形状注释（`(B, T, C)`、`(B, nh, T, hs)` 等），因为否则张量对读者来说是不透明的。他的观点是：这些注释应该由类型检查器推断，而不是手工维护。 Avik 描述了三个构建块： 1. **类型级别的符号算术。** Pyrefly 引入了 `Dim[N]` 类型，它包装一个具体整数（`Dim[8]`）或一个符号整数表达式（`Dim[4 * config.n_embd]`）。类型检查器不嵌入 SAT 求解器；它标准化表达式并检查语法是否匹配。心理模型：`Dim` 之于 `Literal` (https://docs.python.org/3/library/typing.html#typing.Literal) 就像符号整数之于具体整数。 2. **一个 `Tensor` 类型，泛型于可变数量的维度。** `Tensor[B, T, N]` 用于 3D 张量；当维度在静态上未知时使用 `Tensor[*Shape]`。形状来源于张量创建操作，其签名将形状与模型配置中的整数参数绑定。 3. **通过一个微小的形状 DSL 进行操作定型。** PyTorch 有数千个运算符。将每个写成一个类型桩是不可行的，因为形状变换过于丰富。Pyrefly 为每个 PyTorch 操作定义了一个“伪操作”：一个类似推导式的函数，接受整数并返回输出形状。该 DSL 足够小，可以控制成本，并且其精神借鉴自 PyTorch 在 `torch.compile` (https://docs.pytorch.org/docs/stable/torch.compiler_dynamic_shapes.html) 中自身的符号形状工作。 他讲解了几个真实模块的代码示例：一个 MLP 类、一个包含 `chunk(3, dim=-1)` 分割（检查器跟踪生成的三个张量元组）的注意力模块，以及一个带有掩码和形状重塑的标准 scaled-dot-product attention (https://docs.pytorch.org/docs/stable/generated/torch.nn.functional.scaled_dot_product_attention.html) 模式。 在他样本上的覆盖率：每个模型约 450 行代码和 30 个带形状注释的张量，每个模型约 1.5 个 `type: ignore` 注释。大多数覆盖率损失来自常见的 Python 类型化限制（异构列表、列表推导式形状依赖），而非特定于张量的东西。他指出了几个未来工作可以解决的表达能力空白：可整除性约束（系统无法证明 `N * (M // N) == M`）以及作为列表元素的张量，其中元素索引驱动元素类型。 实际的障碍是语法上的，而非理论上的。PEP 695 (https://peps.python.org/pep-0695/) 在定义时急切地求值泛型类的类型参数和基类表达式，因此引用运行时值的 `Dim[4 * config.n_embd]` 将无法与新的泛型语法一起工作。幻灯片列出了一些变通方法：`from __future__ import annotations`、较旧的 `TypeVar` 形式，或者 `jaxtyping` (https://github.com/google/jaxtyping) 风格的字符串注释（所有这些 Pyrefly 已经接受）。他将急切求值规则视为值得推动的杠杆：放松它，张量形状类型就可以无需仪式地编写。 Avik 以一个关于系统上手的轶事结束：当他的团队使用 LLM 代理向新模块添加张量类型时，模型们表示反对，坚称类型系统无法表达他的要求。他不得不指示它们无论如何都要尝试，因为 Pyrefly 中的张量形状类型是最近的，不在训练数据中。 ## Python 的交类型——Jelle Zijlstra 指向标题的链接 (https://bernat.tech/posts/pycon-us-2026-typing-summit-recap/#intersection-types-for-python--jelle-zijlstra) Jelle Zijlstra 的“渐进类型使事情复杂化”幻灯片，显示 Any 作为一个格范围