「类型系统与类型推断」

# 类型用 Python 对象表示
class Ty:
    pass

class TInt(Ty): ...
class TBool(Ty): ...
class TFun(Ty):
    def __init__(self, params: list[Ty], ret: Ty):
        self.params = params
        self.ret = ret

class TVar(Ty):
    """类型变量: 推断时代表"待确定的类型"。"""
    _counter = 0
    def __init__(self):
        TVar._counter += 1
        self.id = TVar._counter
    def __repr__(self):
        return f"t{self.id}"

# 把规则翻译成检查器: 对已知类型做结构匹配
def infer_int_lit(node):  return TInt()
def infer_var(node, gamma):  return gamma[node.name]

def infer_add(node, gamma):
    t1 = infer(node.left, gamma)
    t2 = infer(node.right, gamma)
    if t1 != TInt() or t2 != TInt():
        raise TypeError("+ expects Int operands")
    return TInt()

def infer_fun(node, gamma):
    param_t = TInt() if not node.annotation else node.annotation
    inner = dict(gamma)
    inner[node.param] = param_t
    body_t = infer(node.body, inner)
    return TFun([param_t], body_t)

# 合一: 求解类型等式
def unify(t1, t2, subst):
    t1 = apply(t1, subst)
    t2 = apply(t2, subst)
    if isinstance(t1, TVar):
        if t1 == t2:
            return subst
        if occurs(t1, t2):
            raise TypeError("occurs check failed: infinite type")
        return {**subst, t1.id: t2}
    if isinstance(t2, TVar):
        return unify(t2, t1, subst)
    if isinstance(t1, TInt) and isinstance(t2, TInt):
        return subst
    if isinstance(t1, TFun) and isinstance(t2, TFun):
        subst = unify(t1.ret, t2.ret, subst)
        for p1, p2 in zip(t1.params, t2.params):
            subst = unify(p1, p2, subst)
        return subst
    raise TypeError(f"cannot unify {t1} with {t2}")

# 推断 f = fn(x) -> x + 1 的类型
# 1. x -> TVar t1, 1 -> Int
# 2. t1 + Int  => 约束 t1 = Int
# 3. 结果类型为 Int => f : Int -> Int

# 泛型函数的类型 + 约束的表示
class TForall(Ty):
    """forall a. Constraint[a] => body"""
    def __init__(self, var: TVar, constraint, body: Ty):
        self.var = var
        self.constraint = constraint   # 如 "Clone"
        self.body = body

def instantiate(forall, subst=None):
    """使用时把 forall 的类型变量换成新变量 (多态实例化)。"""
    fresh = TVar()
    return TForall(fresh, forall.constraint,
                   apply(forall.body, {forall.var.id: fresh}))

def solve_constraints(constraints, subst):
    """约束求解: 对每个 (TVar, Trait) 检查实例表。"""
    for var, trait in constraints:
        concrete = apply(var, subst)
        if not impl_table.get((str(concrete), trait)):
            raise TypeError(
                f"type {concrete} does not implement {trait}")
    return subst

// Rust 中约束求解的实际体现: trait bound 被检查器验证
fn min<T: Ord>(a: T, b: T) -> T {
    if a < b { a } else { b }
}
// 使用处: min(1, 2) 要求 i32: Ord —— 编译器查实例表

# 联合类型与子类型的简单实现
class TUnion(Ty):
    def __init__(self, members: list[Ty]):
        self.members = members

class TClass(Ty):
    def __init__(self, name, parent=None):
        self.name = name
        self.parent = parent          # 单继承

SUBTYPING = {}  # 类继承关系表

def is_subtype(sub, sup):
    """判断 sub <: sup"""
    if isinstance(sup, TUnion):
        return all(is_subtype(sub, m) for m in sup.members)
    if isinstance(sub, TUnion):
        return any(is_subtype(m, sup) for m in sub.members)
    if isinstance(sub, TClass) and isinstance(sup, TClass):
        cur = sub
        while cur is not None:
            if cur is sup:
                return True
            cur = cur.parent
        return False
    return sub == sup

# 例: Cat <: Animal, 因此 Cat 可以传给接受 Animal 的函数

class TypeChecker:
    def __init__(self):
        self.gamma = {}          # 符号表: name -> Ty

    def check(self, node):
        match node:
            case {"kind": "int", "value": v}:
                return TInt()
            case {"kind": "var", "name": n}:
                if n not in self.gamma:
                    raise TypeError(f"undefined name: {n}")
                return self.gamma[n]
            case {"kind": "binop", "op": "+", "left": l, "right": r}:
                tl, tr = self.check(l), self.check(r)
                if tl != TInt() or tr != TInt():
                    raise TypeError(f"{l} + {r}: Int expected")
                return TInt()
            case {"kind": "func", "param": p, "ann": t, "body": b}:
                saved = dict(self.gamma)
                self.gamma[p] = t
                bt = self.check(b)
                self.gamma = saved
                return TFun([t], bt)

    def run(self, program):
        for stmt in program:
            self.check(stmt)

def type_error_report(err, source_lines):
    loc = err.location            # 行列号
    line = source_lines[loc.line - 1]
    marker = " " * (loc.col - 1) + "^"
    return (
        f"error[{err.code}]: {err.message}\n"
        f"  --> {err.file}:{loc.line}:{loc.col}\n"
        f"{loc.line:>3} | {line}\n"
        f"     | {marker}\n"
        f"     | expected `{err.expected}`, found `{err.found}`"
    )