混淆Haskell类型推断

Question

我刚开始学习Haskell.由于Haskell是静态类型的并且具有多态类型推断,因此标识函数的类型是

id :: a -> a

建议id可以将任何类型作为其参数并返回自身.我尝试时工作正常:

a = (id 1, id True)

我只是假设在编译时,第一个id是Num a :: a - > a,第二个id是Bool - > Bool.当我尝试以下代码时,它会给出一个错误:

foo f a b = (f a, f b)
result = foo id 1 True

它显示了a的类型必须是相同类型的b,因为它可以正常工作

result = foo id 1 2

但是,如果id的参数类型可以是多态的,那么a和b可以是不同的类型吗？

Answer 1

好吧,这是Haskell类型系统的一个奇怪的怪异角落.这里的问题是有两种方法可以输入你的函数foo.

-- rank 1
foo :: forall a b. (a -> b) -> a -> a -> (b, b)
foo f a b = (f a, f b)

-- rank 2
foo' :: (forall a. a -> a) -> a -> b -> (a, b)
foo' f a b = (f a, f b)

第二种类型是你想要的类型,但第一种类型是你得到的类型.第二种类型,如amalloy所指出的,是一种排名2类型(我们将忽略这两种方式,但如果你想对排名的一个很好的解释,请阅读"任意级别类型的实用类型推断"中的介绍-不要被PDF文件的学术性质所拖延,因为开始是可访问和清晰的书面文件).

我们暂时推迟排名较高的类型的定义,只是说问题是GHC无法推断排名-2类型.引用论文:

已知完整类型推断对于更高级别(impredicative)类型系统是不可判定的,但在实践中,程序员更愿意添加类型注释来指导类型推理引擎,并记录其代码....

Kfoury和Wells表明,对于≤2的等级,可归类性是可判定的,对于所有等级≥3的可归类性是不可判定的(Kfoury&Wells,1994).对于rank-2片段,同一篇论文给出了一种类型推断算法.这种推理算法有点微妙,与用户提供的类型注释不能很好地交互,据我们所知,它还没有在生产编译器中实现.

不可判定意味着没有任何算法总能导致正确的"是或否"决策.所以你有它:不可能推断出3级或更高级别的类型,并且它太难以推断出等级2类型.

现在,回到排名2.这(forall a. a -> a)就是它排名第二的原因.关于forall关键字的含义已经有了一个很好的Stack Overflow问题所以我会引用你的话,但基本上它意味着你能够在拥有和不同类型时调用f a和f b表达,这是你想要的第一个所有这些热点之前的地方.(f a, f b)ab

最后一件事:你通常不会forall在GHCi中看到s 的原因是,forall外部范围内的任何s都被排除在外.所以forall a b. (a -> b) -> a -> a -> (b, b)相当于(a -> b) -> a -> a -> (b, b).

总的来说,这是一个很难解释的语言的痛点.

(在评论中给@amalloy提示.)