Refinement Types：类型不只说“这是整数”，还可以说“它大于 0”

普通类型系统会告诉我们一个值是整数、字符串或用户对象，但很多业务规则比这更细：订单金额必须大于 0，数组下标必须落在范围内，用户名必须符合某种格式。Refinement Type，中文常译为“精化类型”或“细化类型”，就是在基础类型上再附加一个谓词条件。

从“整数”到“满足条件的整数”

Int 只能表达“这是一个整数”。精化类型可以表达“这是一个大于 0 的整数”或“这是一个长度小于 256 的字符串”。如果函数要求接收前一种值，类型检查器或验证工具就有机会在调用点检查这个前提。

这并不意味着所有业务规则都能自动证明。工具通常会把精化条件转成逻辑约束，再交给求解器。如果条件太复杂、涉及外部系统或缺乏足够的函数规格，开发者可能需要提供辅助证明或接受分析器无法确定。

运行时校验是在程序执行时检查条件，例如收到订单后判断金额是否为正。精化类型则尝试把一部分检查提前到编译或验证阶段。两者不是互斥关系：外部输入仍然不可信，需要先验证；一旦验证完成，内部函数可以携带更精确的类型信息，减少重复检查。

LiquidHaskell 是一个典型实践：开发者可以给已有 Haskell 函数补充精化规格，描述返回值与输入之间的关系。这个方式很适合讲清“类型不仅是分类标签，也可以是可检查的契约”。

AI 可能生成一个函数，类型上完全正确，但业务上仍然把负数当价格、空列表当必有元素。精化类型把这些隐含要求显式写出来，帮助人类和工具沟通“正确到底是什么意思”。

但不要把它当成万能护盾。精化规则越复杂，维护和验证成本越高；如果团队没有持续维护规格，类型系统也无法替大家理解业务。

精化类型把“类型正确”推进了一步：不仅知道值属于哪一类，还能表达它必须满足什么条件。它适合把关键业务不变量写成机器可检查的契约。