通过替代统一具有不同成分的涂抹器

【问题标题】：Unification of applicators with different arity through substitution通过替代统一具有不同成分的涂抹器
【发布时间】：2021-05-10 05:53:23
【问题描述】：

我能够统一以下术语：

foo :: (a -> b -> c) -> a -> b -> c
bar :: (a' -> b') -> a' -> b'
foo bar

a ~ (a' -> b')
b ~ a'
c ~ b'

(a' -> b') -> a' -> b'

但我无法为以下统一应用正确的规则，因为 foo 需要一个三元函数，但 bar 只有两个参数：

foo :: (a -> b -> c -> d) -> a -> b -> c -> d
bar :: (a' -> b') -> a' -> b'
foo bar

-- ...?

(a' -> c -> d) -> a' -> c -> d

推断的类型来自 GHCI。我怎么去那里？

【问题讨论】：

【解决方案1】：

因为foo 需要一个三元函数，但bar 只有两个参数

嗯，永远记住，Haskell 根本没有二元或三元函数——它只有一元函数。三元函数实际上是一个一元函数，其结果是一个一元函数，其结果是一个函数。

在这种情况下，bar' 必须通过让b' 成为函数类型来“伪造”一个额外的参数。这是一个特殊版本的 bar：

     -- b' ~ (d -> e)
bar :: (a' -> d -> e) -> a' -> d -> e

瞧，bar 有三个参数。

现在应该清楚如何将它与foo 的参数统一起来。

【讨论】：