name: 精炼类型检查器 description: ‘实现带谓词的精炼类型。使用场景：(1) 属性验证，(2) 轻量依赖类型，(3) 契约。’ version: 1.0.0 tags:

类型系统
精炼类型
验证
smt difficulty: 高级 languages:
python
z3 dependencies:
类型检查器生成器

精炼类型检查器

实现带逻辑谓词的精炼类型。

何时使用

属性验证
契约检查
轻量依赖类型
前置/后置条件

此技能的功能

精炼类型 - 添加谓词到类型
检查子类型 - 通过谓词蕴含
验证 - 使用 SMT 求解器
推断 - 精炼推理

核心理论

精炼类型：
  {x : T | P}    -- T 带谓词 P
  
  示例：
    {x : Int | x > 0}     -- 正整数
    {x : Int | x >= 0 && x < n}  -- 有界整数
    (x : Int) -> {y : Int | y = x + 1}  -- 函数

实现

import z3
from dataclasses import dataclass
from typing import Dict, Optional

@dataclass
class RefinementType:
    """精炼类型 {x : base | pred}"""
    base: 'Type'
    var: str  # 变量名
    predicate: z3.BoolRef

@dataclass
class Type:
    """基类型"""
    pass

@dataclass
class TInt(Type):
    pass

@dataclass
class TFun(Type):
    domain: Type
    codomain: RefinementType

class RefinementChecker:
    """检查精炼类型"""
    
    def __init__(self):
        self.solver = z3.Solver()
        self.env: Dict[str, RefinementType] = {}
    
    def check(self, expr: 'Expr', expected: RefinementType) -> bool:
        """检查表达式是否有精炼类型"""
        
        inferred = self.infer(expr)
        
        # 检查子类型：inferred <: expected
        return self.subtype(inferred, expected)
    
    def infer(self, expr: 'Expr') -> RefinementType:
        """推断精炼类型"""
        
        match expr:
            case Const(n):
                return RefinementType(
                    TInt(),
                    "x",
                    z3.Int('x') == n
                )
            
            case Var(x):
                return self.env.get(x, RefinementType(TInt(), "x", True))
            
            case BinOp('+', e1, e2):
                t1 = self.infer(e1)
                t2 = self.infer(e2)
                
                # 精炼结果
                return RefinementType(
                    TInt(),
                    "r",
                    z3.And(
                        t1.predicate,
                        t2.predicate,
                        z3.Int('r') == z3.Int('e1_val') + z3.Int('e2_val')
                    )
                )
            
            case If(cond, then, else_):
                # 基于条件分支
                t_cond = self.infer(cond)
                t_then = self.infer(then)
                t_else = self.infer(else_)
                
                return RefinementType(
                    t_then.base,
                    "x",
                    z3.Or(
                        z3.And(t_cond.predicate, t_then.predicate),
                        z3.And(z3.Not(t_cond.predicate), t_else.predicate)
                    )
                )
    
    def subtype(self, sub: RefinementType, sup: RefinementType) -> bool:
        """检查 sub <: sup"""
        
        # sub <: sup 当且仅当 ∀x. sub.predicate → sup.predicate
        # (以及基类型兼容)
        
        self.solver.push()
        
        # 替换：重命名变量
        sub_pred = sub.predicate
        sup_pred = sup.predicate
        
        # 检查：sub → sup
        self.solver.add(z3.Not(z3.Implies(sub_pred, sup_pred)))
        
        result = self.solver.check() == z3.unsat
        self.solver.pop()
        
        return result

# 示例：列表长度
def list_length_example():
    """
    // 精炼列表类型
    type List a = Nil | Cons a (List a)
    
    // 带精炼的长度函数
    length : (xs : List a) -> {n : Int | n >= 0}
    length Nil = 0
    length (Cons _ xs) = 1 + length xs
    
    // 类型保证：
    // - 结果非负
    // - 正确长度
    """
    pass

# 示例：排序列表
def sorted_list_example():
    """
    // 排序列表
    SortedList : List Int -> Prop
    SortedList Nil = true
    SortedList (Cons x Nil) = true
    SortedList (Cons x (Cons y ys)) = x <= y && SortedList (Cons y ys)
    
    // 插入排序返回排序列表
    insertSort : (xs : List Int) -> {ys : List Int | SortedList ys}
    
    // 类型保证排序输出
    """
    pass

SMT 编码

class RefinementEncoder:
    """编码精炼到 SMT"""
    
    def encode_type(self, rtype: RefinementType) -> z3.Sort:
        """编码精炼类型"""
        
        # 对于整数精炼：Int
        # 对于更复杂的：未解释排序
        return z3.Int
    
    def encode_predicate(self, rtype: RefinementType) -> z3.BoolRef:
        """编码谓词"""
        
        return rtype.predicate
    
    def encode_subtype(self, sub: RefinementType, sup: RefinementType) -> z3.BoolRef:
        """编码子类型检查"""
        
        # ∀x. sub.pred(x) → sup.pred(x)
        x = z3.Int('x')
        
        return z3.ForAll(
            [x],
            z3.Implies(
                self.substitute(sub.predicate, x),
                self.substitute(sup.predicate, x)
            )
        )

关键概念

概念	描述
精炼	添加谓词到类型
子类型	谓词蕴含
SMT	解决谓词约束
液体类型	精炼 + 推理

液体类型

液体类型推理：
  - 从 Hindley-Milner 获取基类型
  - 从谓词变量获取精炼
  - 解决使用约束
  
  示例：
    length :: xs:[a] -> {v:Int | v = len xs}
    
    约束：
      length [] = {v | v = 0}
      length (y:ys) = {v | v = 1 + length ys}

提示

使用 SMT 求解器
保持谓词简单
利用类型推理
考虑液体类型

标准参考文献

参考文献	重要性
Freeman & Pfenning, “Refinement Types for ML” (PLDI 1991)	原始精炼类型论文
Rondon, Kawaguchi & Jhala, “Liquid Types” (PLDI 2008)	使用 SMT 推理的液体类型
Xi & Pfenning, “Dependent Types in Practical Programming” (PLDI 1999)	DML: 依赖 ML
Vazou et al., “Liquid Haskell: Haskell as a Theorem Prover” (Haskell 2014)	Haskell 中的精炼类型

权衡与限制

精炼类型方法的权衡

方法	优点	缺点
液体类型	自动推理	表达能力有限
完整精炼	表达性强	难以检查
索引类型	类似依赖类型	复杂

何时不使用精炼类型

用于复杂证明：使用完整依赖类型或 Coq
用于运行时检查：常规测试可能更好
用于未知属性：无法表达

复杂性考量

SMT 求解：最坏情况下 NP 难
类型检查：可能昂贵
约束解决：实践中通常快速

限制

表达能力：不是完整依赖类型
SMT 依赖：需要求解器
不可判定性：某些检查不可判定
错误信息：难以解释
可扩展性：大型约束缓慢
终止性：无法证明终止
量词：支持有限

研究工具与工件

精炼类型工具：

工具	语言	学习内容
Liquid Haskell	Haskell	精炼类型
F*	F*	验证
Dafny	Dafny	精炼

研究前沿

1. 液体类型

方法：谓词推理

实现陷阱

陷阱	实际后果	解决方案
SMT 超时	检查缓慢	简化谓词

精炼类型检查器Skill refinement-type-checker

精炼类型检查器

何时使用

此技能的功能

核心理论

实现

SMT 编码

关键概念

液体类型

提示

相关技能

标准参考文献

权衡与限制

精炼类型方法的权衡

何时不使用精炼类型

复杂性考量

限制

研究工具与工件

研究前沿

1. 液体类型

实现陷阱