不同元数应用符的代换统一：Haskell类型推导问题

核心前置规则 #

• 函数类型箭头->是右结合的，比如x -> y -> z等价于x -> (y -> z)；柯里化函数本质是逐层返回函数的嵌套结构。
• 计算f x的类型时，先将f的第一个参数类型与x的类型做全量匹配：两边类型结构必须完全对齐，未绑定的自由类型变量会被临时绑定为对方的结构；匹配完成后，把f返回类型中所有已绑定的变量替换为对应结构，即为f x的最终类型。

简单场景验证（对应你已掌握的推导） #

已知两个类型：
foo :: (a -> b -> c) -> a -> b -> c
bar :: (a' -> b') -> a' -> b'
推导foo bar的类型步骤：

1. 按右结合拆分两边的函数链：
   • foo的第一个参数链：a → (b → c)
   • bar的类型链：(a' → b') → (a' → b')
2. 逐层匹配绑定：
   • 第一层输入对齐：foo的输入a = bar的输入(a' → b')，得到绑定a ~ (a' → b')
   • 第一层返回对齐：foo的返回b → c = bar的返回a' → b'，继续拆分：
     • 第二层输入对齐：foo的输入b = bar返回的输入a'，得到绑定b ~ a'
     • 第二层返回对齐：foo的输入c = bar返回的返回b'，得到绑定c ~ b'
3. 替换绑定关系到foo的返回类型a → b → c，得到结果(a' → b') → a' → b'，和推导一致。

复杂场景推导（对应你卡住的部分） #

已知两个类型：
foo :: (a -> b -> c -> d) -> a -> b -> c -> d
bar :: (a' -> b') -> a' -> b'
推导foo bar的类型步骤：

1. 按右结合拆分两边的函数链：
   • foo的第一个参数链：a → (b → (c → d))
   • bar的类型链：(a' → b') → (a' → b')
2. 第一层匹配（最外层函数）：
   • foo的最外层输入a 对齐 bar的最外层输入(a' → b')，得到绑定a ~ (a' → b')
   • foo的最外层返回b → (c → d) 对齐 bar的最外层返回a' → b'，进入下一层匹配。
3. 第二层匹配（上一层返回的函数）：
   • 这一层foo的输入b 对齐 bar返回的输入a'，得到绑定b ~ a'
   • 这一层foo的返回c → d 对齐 bar返回的返回b'：
     这里是容易卡住的核心：b'是bar自带的自由类型变量，没有预先绑定任何结构，可以直接被绑定为任意类型，包括foo侧的函数结构c → d，因此得到绑定b' ~ (c → d)
4. 替换所有绑定关系到foo的返回类型：
   foo传完第一个参数bar后，剩余的返回类型是原始定义里的a → b → c → d，代入绑定关系替换：
   • 先把a替换为a' → b'，再把b'替换为c → d，因此a最终等价于a' → c → d
   • 再把b替换为a'
     替换完成后得到的类型为(a' → c → d) → a' → c → d，和GHCI的推断结果完全一致。

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