如何在Haskell中实现从输入输出对推导SKI组合子的主类型推断？

我们需要从SKI组合子的输入-输出类型对推导隐藏函数的主类型：已知输入、输出的类型，但无法访问函数本身。SKI组合子的类型定义如下：

k::t1->t2->t1
k x y = x

s::(t1 -> t2 -> t3) -> (t1 -> t2) -> t1 -> t3
s x y z = x z (y z)

i:: t1->t1
i x = x

示例场景 #

比如已知输入类型为k::t1->t2->t1，输出类型为kk::m1->m3->m4->m3，要推导接收该输入并产生对应输出的函数f的最通用类型。这里可以推断出f的类型是f1->f2->f1：因为将f应用到输入类型k::a->b->a时，得到的结果类型是f2->f1，这个类型需要匹配输出的m1->m3->m4->m3，因此f2=m1，f1=m3->m4->m3，完全符合f1->f2->f1的多态模式。

问题：Haskell直接尝试的失败 #

我尝试用Haskell的类型推断直接处理，但遇到了问题：

• 当显式指定f为k时，GHCI能正确推断类型：

  :t (\f -> let x = k in let y = f x in f) k
  -- 输出：(t1 -> t4 -> t1) -> t5 -> t1 -> t4 -> t1
  

• 但当隐藏f，仅指定输入x的类型和f x的输出类型时，GHCI报错：

  :t (\f -> let x = k::a->b->a in let y = (f x)::t5 -> t1 -> t4 -> t1 in f)
  

  错误信息：

  Couldn't match expected type ‘(a0 -> b0 -> a0) -> t2 -> t3 -> t7 -> t3’ with actual type ‘p’ because type variables ‘t2’, ‘t3’, ‘t7’ would escape their scope

实现方案：手动实现Hindley-Milner核心逻辑 #

Haskell的内置类型推断受作用域限制，无法直接处理这种“从约束反推多态类型”的场景。我们需要手动实现合一算法和类型替换，模拟Hindley-Milner类型推断的核心步骤：

1. 定义类型表示

首先用数据结构表示类型：

data Type = Var String
          | Arrow Type Type
          deriving (Eq, Show)

2. 实现合一与替换函数

合一算法用于解决类型间的等式约束，替换函数用于将类型变量替换为具体类型：

-- 合一两个类型，返回类型变量的替换规则（若可合一）
unify :: Type -> Type -> Maybe [(String, Type)]
unify (Var a) (Var b) | a == b = Just []
unify (Var a) t = if a `notElem` freeVars t then Just [(a, t)] else Nothing
unify t (Var a) = unify (Var a) t
unify (Arrow t1 t2) (Arrow t3 t4) = do
  s1 <- unify t1 t3
  s2 <- unify (substitute s1 t2) (substitute s1 t4)
  return (s1 ++ s2)

-- 获取类型中的自由变量
freeVars :: Type -> [String]
freeVars (Var a) = [a]
freeVars (Arrow t1 t2) = freeVars t1 ++ freeVars t2

-- 将替换规则应用到类型上
substitute :: [(String, Type)] -> Type -> Type
substitute subs (Var a) = case lookup a subs of
  Just t -> substitute subs t
  Nothing -> Var a
substitute subs (Arrow t1 t2) = Arrow (substitute subs t1) (substitute subs t2)

3. 推断隐藏函数的主类型

通过约束f 输入类型 ≡ 输出类型，反向推导f的类型：

inferFType :: Type -> Type -> Maybe Type
inferFType inType outType = do
  -- 为f分配初始的多态类型变量：α → β
  let fType = Arrow (Var "α") (Var "β")
  -- 计算f应用输入类型后的结果类型
  let appliedType = substitute [("α", inType)] (Var "β")
  -- 合一结果类型与输出类型，得到替换规则
  subs <- unify appliedType outType
  -- 将替换规则应用到f的初始类型，得到主类型
  return $ substitute subs fType

4. 测试示例

-- 定义输入类型：k的类型 a->b->a
let inType = Arrow (Var "a") (Arrow (Var "b") (Var "a"))
-- 定义输出类型：t5->t1->t4->t1
let outType = Arrow (Var "t5") (Arrow (Var "t1") (Arrow (Var "t4") (Var "t1")))
-- 推断f的类型
inferFType inType outType

输出结果为：

Just (Arrow (Arrow (Var "a") (Arrow (Var "b") (Var "a"))) (Arrow (Var "t5") (Arrow (Var "a") (Arrow (Var "b") (Var "a")))))

即(a->b->a) -> t5 -> (a->b->a)，完全符合我们预期的f1->f2->f1多态模式。

内容的提问来源于Stack Exchange，提问作者Oleg Dats