上下文类型推断系统中递归函数的类型检查问题

你的问题出在当前的Let处理逻辑是先计算e1的类型，再将变量绑定加入上下文，但递归场景下e1会引用自身变量，此时上下文里还没有该变量的类型，必然触发"变量未找到"的错误。

解决核心是先为递归变量分配一个类型占位符（类型变量），将其加入上下文后再检查e1，最后通过类型合一确定占位符的实际类型。具体步骤如下：

1. 扩展Type定义，加入类型变量 #

首先需要在你的Type数据类型中添加类型变量构造器，用于作为递归变量的初始占位：

data Type = Int | Bool | Fun Type Type | TVar String  -- TVar用于类型占位

2. 实现类型合一与替换函数 #

类型合一用于将类型变量与实际类型绑定，替换函数则负责将所有类型变量替换为最终确定的类型：

-- 合一两个类型，返回替换规则列表
unify :: Type -> Type -> [(String, Type)] -> [(String, Type)]
unify (TVar a) t subs = (a, t) : subs
unify t (TVar a) subs = (a, t) : subs
unify (Fun t1 t2) (Fun t1' t2') subs = unify t2 t2' (unify t1 t1' subs)
unify Int Int subs = subs
unify Bool Bool subs = subs
unify t1 t2 _ = error $ "Type mismatch: " ++ show t1 ++ " vs " ++ show t2

-- 将替换规则应用到类型上
applySubs :: [(String, Type)] -> Type -> Type
applySubs subs (TVar a) = case lookup a subs of
                            Just t -> applySubs subs t  -- 递归替换，处理嵌套类型变量
                            Nothing -> TVar a
applySubs subs (Fun t1 t2) = Fun (applySubs subs t1) (applySubs subs t2)
applySubs _ t = t  -- 基础类型直接返回

3. 修改Let表达式的类型检查逻辑 #

调整vt函数，改为返回类型和替换规则（或者用状态传递处理替换），递归Let的处理流程变为：

1. 为递归变量创建新鲜的类型占位符
2. 将占位符绑定加入上下文，检查e1得到类型和替换规则
3. 用替换规则确定占位符的实际类型，更新上下文
4. 用更新后的上下文检查e2

修改后的vt函数示例：

type Ctx = [(String, Type)]

vt :: Ctx -> Expr -> (Type, [(String, Type)])
-- 变量处理逻辑基本不变，返回空替换
vt ctx (Var x) = case lookup x ctx of
                    Just t -> (t, [])
                    Nothing -> error ("Variable not found: " ++ x ++ " in " ++ show ctx)

-- 递归Let的处理逻辑
vt ctx (Let var e1 e2) = 
    let -- 创建唯一的类型占位符
        freshTVar = TVar $ "t_" ++ var
        -- 先把占位符加入上下文，让e1可以引用递归变量
        tempCtx = (var, freshTVar) : ctx
        -- 检查e1，得到它的类型和推导过程中的替换规则
        (e1Type, subs) = vt tempCtx e1
        -- 应用替换规则，得到递归变量的实际类型
        actualType = applySubs subs freshTVar
        -- 用实际类型更新上下文，检查e2
        finalCtx = (var, actualType) : ctx
        (e2Type, e2Subs) = vt finalCtx e2
    in (e2Type, subs ++ e2Subs)

为什么这个方案可行？ #

递归函数的类型检查需要先假设变量存在某个类型，通过类型变量占位实现这一点。在检查e1的过程中，类型变量会被合一规则逐步约束（比如如果递归函数是let f = \x -> f x，类型变量会被约束为Fun t t），最终得到确定的类型，既解决了递归引用的问题，又不需要硬编码具体类型。

如果你不需要处理多态递归，也可以简化为单态场景的实现，但类型变量的方案是通用且符合现代类型检查器设计的标准做法。

内容的提问来源于stack exchange，提问作者Noob25