为什么函数（+）匹配类型（a - > b - > b）？

Question

折叠功能：

从 http://www.seas.upenn.edu/~cis194/spring13/lectures/04-higher-order.html

Prelude> :t (+) 
(+) :: Num a => a -> a -> a 

*Main> fold (0) (+) [1,2,3] 
6 

采取

fold :: b -> (a -> b -> b) -> [a] -> b 
fold z f []  = z 
fold z f (x:xs) = f x (fold z f xs) 

什么用a -> a -> a型型(a -> b -> b)匹配(+)功能？

由于折叠定义接受函数类型(a -> b -> b)这意味着前2个参数(a -> b)必须是不同的类型？

Answer 1

不，它的意思是，a和b可以是不同的，但它不是强制性的它是不同的。在你的情况下，它是一样的。

一个非常简单的例子来传达这一点：

data SomeType a b = Test a b deriving (Show) 

现在ghci：

Answer 2

你在相反的方向所思所想。您不必检查是否+相同或相匹配a -> b -> b，你想要的+类型是专业化a -> b -> b并检查这一点，你必须统一类型。

统一意味着你想看是否+和类型的类型a -> b -> b可以通过重命名的类型变量应相等。

所以+有类型Num x => x -> x -> x。现在让我们忽略类约束，让我们看看我们是否可以匹配功能类型。 类型变成x -> x -> x和a -> b -> b。实际上，如果我们看看它们的实际情况，最好不要使用关联性：x -> (x -> x)和a -> (b -> b)。

->是型构造函数。即它是将一定数量的类型映射到不同类型的函数。在这种情况下，->构造函数将t_1和t_2这两种类型映射到功能类型(->) t_1 t_2（通常由t_1 -> t_2表示）。

所以类型x -> (x -> x)实际上是(->) x ((->) x x)是应用于x并应用于x和x类型构造->类型构造->。 另一种是(->) a ((->) b b)。

统一时，您考虑两种类型的最外层类型构造函数（在这种情况下为->）。如果这不匹配，你不能统一。否则，你不得不统一构造函数的参数。

所以我们必须统一x与a。它们都是类型变量，所以我们可以将其重命名为其中之一。假设我们将a重命名为x。所以现在我们将重命名应用于类型，获得：(->) x ((->) x x)和(->) x ((->) b b)，您会看到现在匹配x和x。

让我们考虑第二个参数。它不是一个类型变量，所以我们必须匹配类型构造函数，这两个都是->。所以我们对这些参数进行递归处理。

我们想要匹配x和b。它们都是类型变量，所以我们可以重命名其中的一个。假设我们将x重命名为b。我们将这种替换应用于类型，获得：(->) b ((->) b b)和(->) b ((->) b b)。现在一切都匹配。因此这两种类型统一。

关于类约束，当我们重命名x与b我们应用替代的约束也因此成为Num x和Num b最后两种类型都Num b => b -> b -> b。

我希望这可以让你更好地理解类型是如何工作的以及如何检查类型。

---

附注：这是haskell在执行类型推断时所做的。它首先分配一个未知函数一个新的类型变量t。然后它使用统一来获得定义它的表达式的类型，并检查与t相关联的类型，这是函数的类型。