精化类型（Refinement Types）

定义

精化类型（refinement types）是在基础类型上附加逻辑谓词得到的类型，形如 {v: Int | v > 0}（正整数）或 {v: [a] | len v == n}（定长列表）。类型检查时，编译器把谓词转化为逻辑验证条件，交给 SMT 求解器（如 Z3）自动判定。

与依赖类型的对比

精化类型可视为依赖类型的受限、可自动化的形式：表达力弱于完整依赖类型，但谓词限定在可判定理论内，多数证明无需人工书写，工程侵入性小得多。

代表系统

Liquid Haskell 在不改语言的前提下为 Haskell 代码叠加精化类型检查；微软研究院的 F* 结合精化类型与效应系统，其成果用于验证 TLS 协议实现等项目；Rust 生态的 Flux 也属此路线。

应用

可静态排除除零、数组越界、违反业务不变量等错误，是「轻量级形式化验证」的主要形态之一。