Pyrefly 是一款快速的 Python 类型检查器，计划在 2025 年底取代 Meta 现有的 Pyre 类型检查器。
Pyrefly 旨在通过 IDE 功能和检查 Python 代码来提高开发速度。
主要特点：
- 类型推断：除了函数参数之外，Pyrefly 可以在大多数位置推断类型。它可以推断变量的类型和返回类型。
- Flow Types：Pyrefly 可以理解程序的控制流以细化静态类型。
- 增量性：Pyrefly 旨在实现模块级的大规模增量性，并优化检查和并行性。
目前正在积极开发中，存在已知问题。如果您发现错误，请提交问题。
Pyrefly 是一款快速的 Python 类型检查器。它计划在 2025 年底取代 Meta 现有的 Pyre 类型检查器。本 README 介绍了 Pyrefly 的基本用法。完整文档及代码检查工具请访问Pyrefly 网站。
Pyrefly 旨在通过 IDE 功能和检查 Python 代码来提高开发速度。
- 类型推断：除了函数参数之外，Pyrefly 可以在大多数位置推断类型。它可以推断变量的类型和返回类型。
- 流类型：Pyrefly 可以理解程序的控制流以细化静态类型。
- 增量性：Pyrefly 旨在实现模块级的大规模增量性，并优化检查和并行性。
如果您有任何问题或想要报告错误，请 创建问题。
请参阅我们的 贡献指南 以获取有关如何为 Pyrefly 做出贡献的信息。
编写 Python 类型检查器时有很多选择。我们从Pyre1、 Pyright和 MyPy中汲取了灵感。以下是一些值得注意的选择：
- 除了函数的参数外，我们在大多数地方都会推断类型。我们确实会推断变量和返回值的类型。例如，
def foo(x): return True的结果等同于你写的def foo(x: Any) -> bool: ...。 - 我们首先尝试推断
[]它的使用类型，然后再进行修复。例如，xs = []; xs.append(1); xs.append("")我们会推断出“xs: List[int]然后”在最后一条语句上出错。 - 我们使用流类型来细化静态类型，例如，
x: int = 4既知道x具有类型int，而且紧接着的下一次使用x也会知道类型是Literal[4]。 - 我们的目标是实现大规模增量（在模块级别）并通过并行性进行优化检查，旨在利用 Rust 的优势使代码更简单一些。
- 我们期望模块具有大型强连接组件，并且不会尝试利用源代码中的 DAG 形状。
设计中有很多细微之处会定期发生变化。但构建棋盘格的基本原理涉及三个步骤：
- 弄清楚每个模块导出的内容。这需要
import *传递性地解决所有语句。 - 对于每个独立的模块，将其转换为绑定，处理所有语句和范围信息（静态和流）。
- 解决这些绑定，可能需要解决其他模块中的绑定。
如果我们遇到不可知的信息（例如递归），我们会Type::Var插入占位符，稍后再填充。
对于每个模块，我们按顺序完整地解决各个步骤。具体来说，我们不会像 Rosyln或 TypeScript那样首先尝试解决某个特定的标识符，也不会使用细粒度的增量式方法（例如Rust Analyzer 使用Salsa）。相反，我们追求的是原始性能和更简单的以模块为中心的设计——如果解决模块中的所有绑定足够快，就无需单独解决单个绑定。
给定程序：
1: x: int = 4
2: print(x)
我们可能会产生以下绑定：
define int@0=from builtins import intdefine x@1=4: int@0use x@2=x@1anon @2=print(x@2)export x=x@2
值得注意的是：
- 关键在于诸如
define（某事物的定义）、use（某事物的用法）和anon（我们需要进行类型检查但不关心其结果的语句）之类的东西。 - 在许多情况下，一个键的值指的是其他键。
export一些键是通过键和import值从其他模块导入的。- 为了消除标识符的歧义，我们使用它们出现的文本位置（在我使用的示例中
@line，但实际上它是文件中的字节偏移量）。
给定程序：
1: x = 1
2: while test():
3: x = x
4: print(x)
我们最终得到了以下绑定：
x@1=1x@3=phi(x@1, x@3)x@4=phi(x@1, x@3)
表达式phi是两个值的连接点，例如phi(int, str) 。我们忽略和int | str之间的区别，因为在本例中没有必要。defineuse
在求解过程中，x@3我们会遇到递归。操作上：
- 我们开始解决
x@3。 - 那就需要我们去解决
x@1。 - 我们解决的
x@1是Literal[1] - 我们开始求解
x@3。但我们目前正在求解x@3，所以我们发明一个新的Var（我们称之为?1）并返回 。 - 我们得出结论，
x@3一定是的Literal[1] | ?1。 - 由于是
?1由引入的，x@3我们记录为?1 = Literal[1] | ?1。我们可以取其可达上限，并得出结论?1 = Literal[1]。 - 我们简化
x@3为仅仅Literal[1]。
