GHC/GHCi意外接受的代码

Question

我不明白为什么这段代码应该传递类型检查:

foo :: (Maybe a, Maybe b)
foo = let x = Nothing in (x,x)

由于每个组件都绑定到同一个变量x,我希望这个表达式最通用的类​​型(Maybe a, Maybe a).如果我使用a where而不是a,我会得到相同的结果let.我错过了什么吗？

Answer 1

简而言之,x得到的概括类型let.这是Hindley-Milner类型推理算法中的关键步骤.

具体而言,let x = Nothing最初指定x类型Maybe t,其中t是新类型变量.然后,类型得到推广,普遍量化其所有类型变量(技术上:除了在其他地方使用的那些,但在这里我们只有t).这导致x :: forall t. Maybe t.请注意,这与...完全相同Nothing :: forall t. Maybe t.

因此,每次我们x在代码中使用时,都会引用可能不同的类型Maybe t,就像Nothing.使用(x, x)与(Nothing, Nothing)此原因相同的类型.

相反,lambda 不具有相同的泛化步骤.相比之下,(\x -> (x, x)) Nothing"only"具有类型forall t. (Maybe t, Maybe t),其中两个组件都被强制为相同类型.这里x再次指定类型Maybe t,带有t新鲜,但不是一般化的.然后(x, x)分配类型(Maybe t, Maybe t).只有在顶级我们才能推广添加forall t,但是在这一点上为时已晚,无法获得异构对.