类型推导：Hindley-Milner 算法实现

Hindley-Milner（HM）类型推导是 ML 系语言（OCaml、Haskell、Rust）类型系统的理论基础。它能在无需类型注解的情况下自动推导出程序中最通用的类型。本文从零实现一个完整的 HM 类型推导器。

一、类型表示

HM 类型系统包含类型变量、基本类型和函数类型。使用 Union-Find 实现类型变量的合一。

type Type struct {
    Kind     TypeKind
    TVar     *TypeVar
    Args     []*Type  // 函数参数类型
    Ret      *Type    // 函数返回类型
}

type TypeVar struct {
    ID    int
    Instance *Type  // 被实例化为的具体类型
}

type TypeKind int
const (
    TyVar   TypeKind = iota  // 类型变量
    TyInt                     // int
    TyBool                    // bool
    TyString                  // string
    TyArrow                   // T1 -> T2
)

二、合一算法

合一是 HM 算法的核心，用于判断两个类型是否兼容，并在兼容时建立类型变量的绑定关系。

func Unify(t1, t2 *Type) error {
    t1 = Prune(t1)
    t2 = Prune(t2)
    if t1.Kind == TyVar && t1.TVar != t2.TVar {
        if OccursIn(t1.TVar, t2) {
            return fmt.Errorf("infinite type: %v occurs in %v", t1, t2)
        }
        t1.TVar.Instance = t2
        return nil
    }
    if t2.Kind == TyVar {
        return Unify(t2, t1)
    }
    if t1.Kind == TyArrow && t2.Kind == TyArrow {
        if err := Unify(t1.Args[0], t2.Args[0]); err != nil {
            return err
        }
        return Unify(t1.Ret, t2.Ret)
    }
    if t1.Kind == t2.Kind {
        return nil
    }
    return fmt.Errorf("type mismatch: %v vs %v", t1, t2)
}

func Prune(t *Type) *Type {
    if t.Kind == TyVar && t.TVar.Instance != nil {
        t.TVar.Instance = Prune(t.TVar.Instance)
        return t.TVar.Instance
    }
    return t
}

三、类型推导规则

HM 算法使用类型环境 Γ 记录变量到类型的映射，通过递归遍历 AST 推导每个表达式的类型。

type TypeEnv struct {
    parent *TypeEnv
    bindings map[string]*Type
}

func Infer(env *TypeEnv, expr Expr) (*Type, error) {
    switch e := expr.(type) {
    case *IntExpr:
        return NewType(TyInt), nil
    case *VarExpr:
        if t, ok := env.Lookup(e.Name); ok {
            return t, nil
        }
        return nil, fmt.Errorf("unbound variable: %s", e.Name)
    case *LambdaExpr:
        argType := NewTypeVar()
        newEnv := env.Extend(e.Arg, argType)
        retType, err := Infer(newEnv, e.Body)
        if err != nil {
            return nil, err
        }
        return NewArrowType(argType, retType), nil
    case *AppExpr:
        fnType, err := Infer(env, e.Fn)
        if err != nil {
            return nil, err
        }
        argType, err := Infer(env, e.Arg)
        if err != nil {
            return nil, err
        }
        retType := NewTypeVar()
        if err := Unify(fnType, NewArrowType(argType, retType)); err != nil {
            return nil, err
        }
        return retType, nil
    case *LetExpr:
        valType, err := Infer(env, e.Value)
        if err != nil {
            return nil, err
        }
        // 泛化：将自由类型变量提升为多态类型
        scheme := Generalize(env, valType)
        newEnv := env.Extend(e.Name, scheme)
        return Infer(newEnv, e.Body)
    }
    return nil, fmt.Errorf("unknown expression")
}

四、Let 多态

HM 算法的精髓在于 Let 多态：let 绑定的变量可以被泛化为多态类型，每次使用时实例化为新的类型变量。这使得 let id = λx.x in (id 1, id true) 可以通过类型检查。

func Generalize(env *TypeEnv, t *Type) *Scheme {
    freeVars := t.FreeTypeVars()
    envVars := env.FreeTypeVars()
    quantified := setDifference(freeVars, envVars)
    return &Scheme{Vars: quantified, Type: t}
}

func Instantiate(scheme *Scheme) *Type {
    subst := make(map[int]*Type)
    for _, tv := range scheme.Vars {
        subst[tv.ID] = NewTypeVar()
    }
    return ApplySubst(subst, scheme.Type)
}

五、实际应用与局限

HM 算法在 OCaml、Haskell 和 Rust 的类型推导中发挥核心作用。但它也有局限：不支持子类型、不支持高阶类型（需要 System F），且错误信息往往难以理解。现代语言在 HM 基础上做了大量扩展。