Pyrefly

Pyrefly

访问网站

Pyrefly 是一款快速的 Python 类型检查器，计划在 2025 年底取代 Meta 现有的 Pyre 类型检查器。

Pyrefly 旨在通过 IDE 功能和检查 Python 代码来提高开发速度。

主要特点：

类型推断：除了函数参数之外，Pyrefly 可以在大多数位置推断类型。它可以推断变量的类型和返回类型。
Flow Types：Pyrefly 可以理解程序的控制流以细化静态类型。
增量性：Pyrefly 旨在实现模块级的大规模增量性，并优化检查和并行性。

Pyrefly：Python 的快速类型检查器和 IDE

目前正在积极开发中，存在已知问题。如果您发现错误，请提交问题。

Pyrefly 是一款快速的 Python 类型检查器。它计划在 2025 年底取代 Meta 现有的 Pyre 类型检查器。本 README 介绍了 Pyrefly 的基本用法。完整文档及代码检查工具请访问Pyrefly 网站。

入门

Pyrefly 旨在通过 IDE 功能和检查 Python 代码来提高开发速度。

在浏览器中尝试 pyrefly：沙盒
获取命令行工具：pip install pyrefly
获取 VSCode 扩展：链接

主要特点：

类型推断：除了函数参数之外，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 int
define x@1=4: int@0
use x@2=x@1
anon @2=print(x@2)
export x=x@2

值得注意的是：

关键在于诸如define（某事物的定义）、use（某事物的用法）和anon（我们需要进行类型检查但不关心其结果的语句）之类的东西。
在许多情况下，一个键的值指的是其他键。
export一些键是通过键和import 值从其他模块导入的。
为了消除标识符的歧义，我们使用它们出现的文本位置（在我使用的示例中@line，但实际上它是文件中的字节偏移量）。

示例`Var`

给定程序：

1: x = 1
2: while test():
3:     x = x
4: print(x)

我们最终得到了以下绑定：

x@1=1
x@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]。