我怎样才能证明这种类型会被推断出来？

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的参数是natas函数,并且nat具有参数类型a.因此2,nat需要的类型和参数必须相同.

现在我们head用as作为参数调用(nat 2),这意味着我们推理:

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

而且我们知道,a ~ b因为nat 2is 的类型[a]和第一个参数head应该有类型[b].所以这意味着,因为a ~ b,这意味着类型约束Num a,也意味着Num b,反之亦然.

所以类型是:

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