我如何证明会推断出这种类型？

Question

我要复习一下，Haskel 类型推断对我来说有点棘手，尽管它看起来很简单。

给定这个函数：nat x = x : ( nat (x+1))

类型：Num t => t -> [t]

这很清楚，因为 nat 函数接受一个元素并构造一个无限列表。

但是，现在我被要求指定head (nat 2)的类型

我完全理解head :: [a] -> a的原因和类型是什么

但为什么是head (nat 2) :: Num c => c 有人能解释一下原因吗？

从最通用的类​​型开始，即 A -> B（我假设它的 A -> B 因为它需要一个参数）接下来是什么？

编辑

这个Give the type of the expression: head (nat 2)表示我应该给出函数的类型，或者只是返回的值，实际上它必须是一个数字，这就是为什么它是Num c => c，我刚刚回答了我的问题吗？

原问题：Give the type of the expression: head (nat 2)

证明你的答案。

谢谢

Answer 1

让我们假设我们已经导出了nat 的类型并且我们知道head :: [a] -> a 的类型

nat :: Num a => a -> [a]
head :: [b] -> b

然后我们使用不同的类型变量名称a 和b，因为现在我们对a 和b 一无所知，因此我们假设 可以 是不同，因此分配不同的名称。

现在我们在表达式中看到(nat 2)。我们知道2 有类型：

2 :: Num c => c

这意味着nat 2 具有类型：

nat     :: Num a => a -> [a]
2       :: Num c => c
----------------------------
(nat 2) :: Num a =>      [a]

我们知道a ~ c（a 和c 是同一类型）。我们知道这一点，因为2 是函数调用的参数，nat 作为函数，nat 作为参数类型a。因此2的类型和nat的参数需要相同。

现在我们用 (nat 2) 作为参数调用 head，这意味着我们的理由是：

head         ::          [b] -> b
(nat 2)      :: Num a => [a]
---------------------------------
head (nat 2) :: Num b =>        b

我们知道a ~ b，因为nat 2 的类型是[a]，而head 的第一个参数应该是[b] 类型。所以这意味着既然a ~ b，那就意味着类型约束Num a，也意味着Num b，反之亦然。

所以类型是：

head (nat 2) :: Num b => b