约束求解与类型类

-- 源程序
f x = x + 1

-- 生成的约束
--   f 的类型记为 t0，x 的类型记为 t1
--   约束 1: t0 = t1 -> t2         (f 是一个函数)
--   约束 2: Num t1                 (x 必须支持加法)
--   约束 3: Num t2, t2 = t1        (结果与操作数同类型)

# 算法 W 的骨架
def infer(env, expr):
    if is_literal(expr):
        return fresh_type_var()
    if is_var(expr):
        return instantiate(env[expr.name])          # 泛化类型实例化
    if is_lambda(expr):
        tv = fresh_type_var()
        body = infer(env.extend(expr.param, tv), expr.body)
        return Func(tv, body)                       # t_param -> t_body
    if is_apply(expr):
        tf = infer(env, expr.func)
        ta = infer(env, expr.arg)
        tr = fresh_type_var()
        unify(tf, Func(ta, tr))                     # 生成并消解方程
        return tr
    if is_let(expr):
        ta = infer(env, expr.value)
        return infer(env.extend(expr.name, generalize(env, ta)), expr.body)

# 合一的并查集实现：解 t1 = t2 这类方程
def unify(t1, t2):
    t1, t2 = prune(t1), prune(t2)      # 先沿已绑定的链找到代表元
    if t1 is t2:
        return
    if isinstance(t1, TypeVar):
        t1.bind(t2)                    # 绑定，同时做 occurs check
    elif isinstance(t2, TypeVar):
        t2.bind(t1)
    elif same_ctor(t1, t2):
        for a, b in zip(t1.args, t2.args):
            unify(a, b)                # 结构递归
    else:
        raise UnifyError(t1, t2)

class Eq a where
  (==) :: a -> a -> Bool

instance Eq Int where
  (==) = primIntEq

instance Eq a => Eq [a] where       -- 实例本身带约束
  []     == []     = True
  (x:xs) == (y:ys) = x == y && xs == ys
  _      == _      = False

# 约束化简的三条规则
def simplify(constraints):
    # 规则 1：等式直接替换，代入其他约束
    for eq in equations(constraints):
        apply_subst(eq.var, eq.rhs, constraints)
    # 规则 2：可由局部实例立即解决的谓词直接解决
    for p in predicates(constraints):
        if p.is_solved_by_local_instance():
            constraints.resolve(p)
    # 规则 3：无法解决的谓词泛化，进入类型方案的上下文
    return constraints.remaining()

-- 化简示例
f x = show (x + 1)
-- 生成：t0 = t1 -> t2, Num t1, Show t2, t1 = t2
-- 代入 t1 = t2 后：Num t2, Show t2
-- 泛化：f :: (Num a, Show a) => a -> String

# GHC 的约束求解过程可以用 -ddump-tc-trace 观察
ghc -ddump-tc-trace -dsuppress-all Foo.hs 2>&1 | head -60

trait Shape {
    fn area(&self) -> f64;
}

impl Shape for Circle {
    fn area(&self) -> f64 { std::f64::consts::PI * self.r * self.r }
}

fn total_area<S: Shape>(shapes: &[S]) -> f64 {
    shapes.iter().map(|s| s.area()).sum()      // 静态分派：内联后无虚调用
}

// 动态分派：类型擦除成 trait object，走虚表
fn total_area_dyn(shapes: &[Box<dyn Shape>]) -> f64 {
    shapes.iter().map(|s| s.area()).sum()
}

// 单态化：编译器为每个具体类型生成一份代码
// total_area::<Circle> 与 total_area::<Square> 是两个独立函数
// 代价：代码体积膨胀（monomorphization bloat）

trait Iterator {
    type Item;                       // 关联类型：输出
    fn next(&mut self) -> Option<Self::Item>;
}

impl Iterator for Counter {
    type Item = u32;
    fn next(&mut self) -> Option<u32> { /* ... */ }
}

// 使用：编译器必须解出 <Counter as Iterator>::Item = u32
fn sum_all<I: Iterator<Item = u32>>(it: I) -> u32 { /* ... */ }

// 关联类型的约束生成
//   I: Iterator              (谓词)
//   <I as Iterator>::Item = u32   (投影等式)
// 求解时先找 I 的实例，再由实例的 type Item 代入投影等式

原始求解失败信息：
  cannot unify t3 with t7
  约束 t3 = List(t5) 来自第 12 行
  约束 t7 = Int      来自第 15 行

翻译后的用户信息：
  error: expected List(a), found Int
    --> src/main.rs:12:5
     |
  12 |     process(items)      <- 这里传入的是 Int，但函数要求 List
     |             ^^^^^ expected List(a), found Int
     |
  note: process 的参数类型由 src/main.rs:8 定义

-- 歧义约束的诊断：编译器知道有谓词解不出，但不知道用户想要哪个
-- 错误：Ambiguous type variable 'a0' arising from a use of 'show'
-- 建议：加类型标注 (show (read s :: Int))
main = putStrLn (show (read "42"))      -- 无法确定 read 的返回类型

// 实例缺失的诊断：明确告诉用户缺少哪个 impl
// error[E0277]: the trait bound `Circle: Clone` is not satisfied
#[derive(Clone)]
struct Circle { r: f64 }        // 加上 derive 即可修复

// 陷阱：单态化体积爆炸
fn process<T: Display>(x: T) { println!("{}", x); }
// 被 100 个不同类型调用 -> 生成 100 份机器码
// 对策：把不依赖 T 的部分提取到非泛型函数
fn process<T: Display>(x: T) {
    let s = x.to_string();       // 泛型部分只做转换
    process_str(&s);             // 公共部分只编译一份
}
fn process_str(s: &str) { /* 体积大的逻辑 */ }

-- 陷阱：约束求解顺序导致的假歧义
-- 若先解析 Show a 再消等式 a = Int，会误报歧义
-- 正确做法：等式优先消元，再解析谓词

# 观察单态化产物体积
cargo bloat --release --crates        # 按 crate 看体积占比
cargo bloat --release -n 20           # 看最大的 20 个符号