求教Haskell中lambda表达式与高阶函数的类型推导方法

Haskell的类型推导基于辛德雷-米尔纳（Hindley-Milner）算法，核心逻辑是先给所有未知类型分配临时变量，再根据表达式的语法规则提取类型约束，联立约束替换变量后就能得到最通用的主类型，通用推导步骤如下：

• 给所有参数、子表达式分配临时类型变量
• 从最内层表达式开始提取约束：
  • 若存在函数应用a b，则a的类型必然是t1 -> t2，b的类型为t1，应用结果类型为t2
  • 列表的所有元素类型必须完全一致
  • 函数组合a.b的输入类型与b的输入类型一致，输出类型与a的输出类型一致，且b的输出类型等于a的输入类型
• 联立所有约束替换类型变量，消去所有临时变量后得到最终类型

示例1：推导f = (\x -> \y -> \z -> [x (y z), y z])的类型 #

1. 初始化临时变量：x :: a，y :: b，z :: c，返回值类型为d，f的初始类型为a -> b -> c -> d
2. 分析最内层y z：属于函数应用，因此y的类型为c -> e，y z的结果类型为e，得到约束b = c -> e
3. 分析x (y z)：属于函数应用，因此x的输入类型为e；又因为x (y z)和y z属于同一个列表，二者类型必须一致，所以x的输出类型也为e，得到约束a = e -> e
4. 列表元素类型为e，因此返回值类型d = [e]
5. 替换所有约束后得到最终类型：(e -> e) -> (c -> e) -> c -> [e]，替换为常规变量名即(a -> a) -> (b -> a) -> b -> [a]

示例2：推导g = \x -> \y -> \z -> x.y.z的类型 #

1. 已知函数组合运算符(.) :: (b -> c) -> (a -> b) -> a -> c，初始化临时变量：x :: a，y :: b，z :: c，g的初始类型为a -> b -> c -> d
2. 分析y.z：属于函数组合，因此z的类型为c1 -> c2，y的类型为c2 -> c3，y.z的类型为c1 -> c3，得到约束c = c1 -> c2、b = c2 -> c3
3. 分析x.(y.z)：属于函数组合，因此x的类型为c3 -> c4，x.y.z的类型为c1 -> c4，得到约束a = c3 -> c4、d = c1 -> c4
4. 替换所有约束后得到最终类型：(c3 -> c4) -> (c2 -> c3) -> (c1 -> c2) -> c1 -> c4，替换为常规变量名即(a -> b) -> (c -> a) -> (d -> c) -> d -> b

示例3：推导h = foldr (&&)的类型 #

1. 已知基础函数类型：foldr :: (a -> b -> b) -> b -> [a] -> b，(&&) :: Bool -> Bool -> Bool
2. foldr的第一个参数要求类型为a -> b -> b，与(&&)的类型联立得到约束a = Bool、b = Bool
3. 给foldr传入第一个参数后，剩余参数类型为原foldr类型去掉第一个参数，代入约束后得到Bool -> [Bool] -> Bool，即为h的类型

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