Dart中的证明类型：使用final类作为计算见证

# Dart 中的证明类型：使用 final 类作为计算凭证 来源：https://modulovalue.com/blog/proof-types-in-dart/ 以下是 Dart 3.0 实现的一种模式： ```dart final class EmailValidated { const EmailValidated._(); } EmailValidated? validateEmail(String email) { if (_isValidEmail(email)) { return const EmailValidated._(); } return null; } ``` 如果你有一个 `EmailValidated` 实例，那么验证一定已经发生过。此库之外的任何代码都无法绕过 `validateEmail` 凭空产生一个 `EmailValidated` 实例。类型系统强制执行这一点。 我称它们为**证明类型**。其他人称它们为见证类型或证据类型。无论名称如何，其理念相同：值的存在证明了某个计算已经发生。 ## 目录 - 为什么有效（https://modulovalue.com/blog/proof-types-in-dart/#why-this-works） - 更完整的示例（https://modulovalue.com/blog/proof-types-in-dart/#a-more-complete-example） - 携带数据的证明（https://modulovalue.com/blog/proof-types-in-dart/#carrying-data-with-proofs） - 授权检查（https://modulovalue.com/blog/proof-types-in-dart/#authorization-checks） - 其他语言呢？（https://modulovalue.com/blog/proof-types-in-dart/#what-about-other-languages） - 解析，而非验证（https://modulovalue.com/blog/proof-types-in-dart/#parse-dont-validate） - Curry–Howard 对应（https://modulovalue.com/blog/proof-types-in-dart/#the-curry-howard-correspondence） - 何时使用证明类型（https://modulovalue.com/blog/proof-types-in-dart/#when-to-use-proof-types） - 局限性（https://modulovalue.com/blog/proof-types-in-dart/#limitations） - 结论（https://modulovalue.com/blog/proof-types-in-dart/#conclusion） - 补充说明（https://modulovalue.com/blog/proof-types-in-dart/#addendum） ## 为什么有效 四个因素共同促成了这一点： 1. `final` 阻止了该类在其库之外被扩展、实现或混入（参见我关于类修饰符的文章（https://modulovalue.com/blog/understanding-dart-class-modifiers-lattices/））。 2. 库私有构造函数（`._()`）阻止了在库外部实例化。 3. Dart 基于库的隐私机制意味着这些限制是绝对的，而非建议性的。 4. 健全的类型系统（静态和动态）确保类型无法被伪造。Dart 的不安全构造（如 `as` 转换）在运行时会大声失败，而不是无声地产生无效值。 你不可能意外地得到一个假的 `EmailValidated`。那么，获取 `EmailValidated` 实例的**唯一**方式就是调用 `validateEmail()` 并传入一个能通过验证的输入。 ## 更完整的示例 让我们构建一个用户注册系统，其中类型系统强制所有检查都已通过： ```dart // registration_proofs.dart /// 证明电子邮件地址已通过验证。 final class EmailChecked { final String email; const EmailChecked._(this.email); } /// 证明密码满足强度要求。 final class PasswordChecked { const PasswordChecked._(); } /// 证明服务条款已被接受。 final class TermsAccepted { const TermsAccepted._(); } /// 证明所有注册要求均已满足。 final class RegistrationReady { final String email; const RegistrationReady._(this.email); } EmailChecked? checkEmail(String email) { final regex = RegExp(r'^[^@]+@[^@]+\.[^@]+$'); if (regex.hasMatch(email)) { return EmailChecked._(email); } return null; } PasswordChecked? checkPassword(String password) { if (password.length >= 12) { return const PasswordChecked._(); } return null; } TermsAccepted? checkTermsAccepted(bool accepted) { if (accepted) { return const TermsAccepted._(); } return null; } RegistrationReady? prepareRegistration( EmailChecked email, PasswordChecked password, TermsAccepted terms, ) { // 所有检查均已证明通过。我们可以信任这些值。 return RegistrationReady._(email.email); } ``` 现在注册函数： ```dart // registration_service.dart import 'registration_proofs.dart'; void register(RegistrationReady proof) { // 此函数无法被调用，除非： // 1. 电子邮件已验证 // 2. 密码已检查 // 3. 条款已接受 // // 编译器强制执行这一点。文档和代码审查无法做到。 createAccount(proof.email); } ``` 调用者无法直接构造 `RegistrationReady` 实例。他们必须经过 `prepareRegistration()`，该函数需要三个证明类型，而这三个类型只能通过各自的检查获得。 ## 携带数据的证明 证明类型可以携带已验证的数据： ```dart final class ParsedInt { final int value; const ParsedInt._(this.value); } ParsedInt? parseInt(String input) { final result = int.tryParse(input); if (result != null) { return ParsedInt._(result); } return null; } ``` 现在 `ParsedInt` 既是解析成功的证明，也是解析值的载体。 这种模式同样适用于授权： ```dart final class Authorized<T> { final T resource; const Authorized._(this.resource); } Authorized<Document>? authorizeDocumentAccess( User user, Document document, ) { if (user.canAccess(document)) { return Authorized._(document); } return null; } void deleteDocument(Authorized<Document> proof) { // 授权检查已证明发生。无需再次检查。 proof.resource.delete(); } ``` ## 其他语言呢？ 这种模式要求能够创建无法在其定义模块之外实例化的类型。让我们看看哪些语言支持这一点。 ### JavaScript JavaScript 没有这种机制。类总是可以被实例化的： ```javascript class Validated { #private = true; // 私有字段，但是…… constructor() {} // 构造函数始终可访问 } // 任何人都可以这样做： new Validated(); ``` 即使有私有字段，也无法阻止构造。该语言根本没有密封类型的概念。 ### TypeScript TypeScript 的类型系统在运行时被擦除。私有构造函数存在，但不提供运行时保证： ```typescript class Validated { private constructor() {} static create(): Validated { return new Validated(); } } // TypeScript 在编译时阻止： // new Validated(); // 错误 // 但在运行时，它只是 JavaScript： // 任何能访问转译后代码的人都可以绕过 ``` 更根本的是，TypeScript 使用结构类型。任何具有正确形状的对象都满足接口： ```typescript interface Validated { readonly _brand: unique symbol; } // 你仍然可以创建匹配的对象： const fake = { _brand: Symbol() } as Validated; ``` 品牌类型是一种变通方法，但它们并非强制性的。它们依赖于开发者不绕过它们。 ### Python Python 的理念是“我们都是成年人”。没有任何东西是真正私有的： ```python class Validated: def __init__(self): pass # “私有”仅按约定 class _Validated: def __init__(self): pass # 任何人仍然可以这样做： _Validated() # 正常工作 ``` 即使使用 `__slots__`、元类或 `__new__` 技巧，坚定的代码总能创建实例。 ### Java Java 有 `final` 类和私有构造函数： ```java public final class Validated { private Validated() {} public static Validated create() { return new Validated(); } } ``` 这看起来很有希望，但 Java 有反射： ```java Constructor<Validated> constructor = Validated.class.getDeclaredConstructor(); constructor.setAccessible(true); // 绕过私有 Validated fake = constructor.newInstance(); // 创建实例 ``` `setAccessible(true)` 调用绕过了所有访问控制。除非你运行在一个严格的安全管理器下（几乎没有人这样做，而且它自 Java 17 起已被弃用），否则私有构造函数不提供任何保证。 ### Kotlin、Scala、C# 和 PHP 这些语言中重复着同样的故事。Kotlin 和 Scala 运行在 JVM 上，继承了其反射；C# 有 .NET 反射；PHP 有自己的反射 API。在每种情况下，等效于 Java 的 `setAccessible(true)` 的机制都能强制访问私有构造函数，因此保证是建议性的而非强制性的。 ### Go Go 的未导出类型（小写名称）只能在其包内使用： ```go package validation type validated struct { value string } func Validate(input string) *validated { if isValid(input) { return &validated{value: input} } return nil } ``` 这实际上对基本场景有效。外部包无法直接创建 `validated` 实例。然而，Go 的类型系统有局限性。接口是结构的而非名义的，并且 `unsafe` 包可以绕过保护。它更接近我们想要的，但不如 Dart 的方法干净。 ### C C 没有类，但你可以使用不透明指针：在头文件中声明一个结构体而不定义它，只暴露返回指向该结构体指针的函数。外部代码无法直接分配该结构体。但是，C 缺乏类型安全，因此你可以将任何内容转换为任何内容。一次 `memcpy` 或指针转换就足以让你的保证化为乌有。 ### C++ C++ 有 `final` 类（自 C++11 起）和私有构造函数。与 Java 不同，C++ 没有可以绕过访问控制的运行时反射。然而，`friend` 声明会在封装上打洞，而指针算术或 `reinterpret_cast` 可以伪造任何类型。如果你信任你的代码库不会做不安全的事情，C++ 可以近似实现证明类型，但语言本身并不强制执行。 ### Ruby Ruby 是动态且开放的。类可以被重新打开，方法可以被重新定义，`send` 可以调用私有方法。没有什么是真正密封的。 ### Swift Swift 可以实现这种模式： ```swift public final class Validated { fileprivate init() {} } public func validate() -> Validated? { // 只有此文件可以创建 Validated return Validated() } ``` 使用 `final` 防止子类化，以及 `fileprivate`/`private` 防止构造，Swift 提供了与 Dart 类似的保证。Swift 的反射（Mirror）是只读的，但 `unsafeBitCast` 仍然可以从任意位中伪造一个实例。就像在 Rust 中一样，这需要刻意去使用一个明确不安全的 API。 ### Rust Rust 通过其模块系统处理这一点： ```rust mod validation { pub struct Validated { value: String, // 私有字段 } impl Validated { pub fn new(input: &str) -> Option<Validated> { if is_valid(input) { Some(Validated { value: input.to_string() }) } else { None } } } } // 在模块之外，你无法构造 Validated， // 因为你无法访问私有字段。 ``` Rust 的模块系统和私有字段使这种模式变得自然。唯一的逃生舱是 `unsafe`：`std::mem::transmute` 或 `std::mem::zeroed` 可以伪造一个具有私有字段的值。但这意味着写出 `unsafe` 这个词，这是一个响亮、可 grep 的信号，普通代码从不使用。 ### Haskell Haskell 开创了许多此类想法。 ```haskell module Validation (Validated, validate) where newtype Validated = Validated String validate :: String -> Maybe Validated validate input | isValid input = Just (Validated input) | otherwise = Nothing ``` 通过不导出 `Validated` 的构造函数，外部代码无法创建该类型的值。这种模式在 Haskell 中已经被使用了数十年。唯一漏洞是 `unsafeCoerce`，它可以凭空造出一个 `Validated`。就像 Rust 的 `unsafe` 和 Swift 的 `unsafeBitCast` 一样，这是一个明确的、不可错认的逃生舱，而不是正常代码会偶然触及的东西。 ### OCaml gasche 指出（https://www.reddit.com/r/ProgrammingLanguages/comments/1uyv0pv/comment/oy56gyq/），OCaml 属于 ML 家族，具有比 Haskell 更丰富的模块系统，提供了两种实现方式。第一种模仿了 Haskell 的方法：在模块签名中将类型保持为抽象类型。 ```ocaml module Email : sig type validated val validate : string -> validated option val to_string : validated -> string end = struct type validated = string let validate s = if is_valid_email s then Some s else None let to_string s = s end ``` 在模块内部，`validated` 只是一个 `string`，但签名隐藏了这一点。外部代码需要 `Email.to_string` 来读取载荷，并且无法自行构造 `validated`。 第二种方法在 Dart 中没有对应物：私有类型缩写（private type abbreviation）。 ```ocaml module Email : sig type validated = private string val validate : string -> validated option end = struct type validated = string let validate s = if is_valid_email s then Some s else None end ``` 这里 `validated` 是 `string` 的单向子类型。你可以使用 `(x :> string)` 将 `validated` 降级为 `string` 并免费读取载荷，但你无法反向操作，因此获得 `validated` 的唯一方式是通过 `validate`。与完全抽象类型相比，这种保证的仪式感更少。两者都只能被 `Obj.magic`（OCaml 的 `unsafeCoerce`）所破坏。它可以将任何值转换为任何类型并完全跳过构造函数，因此，正如在其他语言中一样，伪造一个证明需要那明确的不安全一步。 ### 总结 | 语言 | 是否可能实现证明类型？ | 原因/原因不 | |----------|------------------------|---------------------| | JavaScript | 否 | 对构造没有访问控制 | | TypeScript | 否 | 类型被擦除，结构类型 | | Python | 否 | 一切可访问，动态类型 | | Java | 否 | 反射绕过私有 | | Kotlin | 否 | JVM 反射绕过私有 | | C# | 否 | 反射绕过私有 | | Go | 部分 | 未导出可行，但 `unsafe` 存在 | | C | 否 | 指针转换绕过一切 | | C++ | 部分 | 无反射，但 `friend` 和转换存在 | | Scala | 否 | JVM 反射绕过私有 | | Ruby | 否 | 动态，类可重新打开 | | PHP | 否 | 反射绕过私有 | | Swift | 是 | `final` + private init，无绕过反射 | | Rust | 是 | 私有字段，强模块系统 | | Haskell | 是 | 模块导出控制构造 | | OCaml | 是 | 抽象或私有类型控制构造 | | Dart | 是 | `final` + 私有构造函数，mirrors 已弃用并禁用 | Dart 与 Swift、Rust、Haskell 和 OCaml 一起提供了这种能力。Dart 确实有反射，通过 `dart:mirrors`，但 mirrors 已被弃用，在 Flutter 中默认禁用，并且在编译到 JavaScript 时不可用。实际上，Dart 代码无法绕过私有构造函数。 一个诚实的说明：标记为“是”的语言并非绝对严密。每种语言都有一个故意设计的不安全逃生舱：Rust 的 `transmute`，Swift 的 `unsafeBitCast`，Haskell 的 `unsafeCoerce`，OCaml 的 `Obj.magic`，以及 Dart 已禁用的 `dart:mirrors`。与“否”语言的区别不在于伪造是否可能，而在于伪造需要显式调用一个不安全操作，而不是普通的反射或正常的类型化代码。 Dart 的显著之处在于它是一种主流的、易于访问的语言，可以随处运行（Web、移动、桌面、服务器），同时仍然提供这些保证。你不需要学习系统语言或函数式语言就能使用证明类型。 ## 解析，而非验证 证明类型体现了“解析，而非验证”的原则（https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-validate/）。 验证会检查数据是否有效，并返回布尔值或抛出异常。数据保持其原始类型： ```dart bool isValidEmail(String email) { return RegExp(r'^[^@]+@[^@]+\.[^@]+$').hasMatch(email); } void processEmail(String email) { if (!isValidEmail(email)) { throw ArgumentError('Invalid email'); } // email 仍然只是一个 String // 没有任何东西阻止你将未验证的字符串传递到这里 } ``` 问题：你可能会忘记调用验证器，或者调用它但忽略结果，或者将一个未验证的字符串传递给期望验证后字符串的函数。类型系统不会提供帮助。 解析会将数据转换为一种新类型，其中有效性编码在类型本身中： ```dart final class ValidEmail { final String value; const ValidEmail._(this.value); } ValidEmail? parseEmail(String email) { if (RegExp(r'^[^@]+@[^@]+\.[^@]+$').hasMatch(email)) { return ValidEmail._(email); } return null; } void processEmail(ValidEmail email) { // 只能以 ValidEmail 调用 // 而 ValidEmail 只能通过成功解析获得 } ``` 现在类型系统强制 `processEmail` 只接收经过验证的电子邮件。你不能忘记验证，因为类型不匹配。你不能传递原始字符串，因为编译器拒绝。