时间戳

首页 > 解决方案 > GHC/GHCi 意外接受的代码

haskell - GHC/GHCi 意外接受的代码

问题描述

我不明白为什么这段代码应该通过类型检查：

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

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

标签： haskellghctype-inferencetypechecking

解决方案

简而言之， 的类型x被 泛化let。这是Hindley-Milner类型推理算法中的关键步骤。

具体来说，let x = Nothing最初分配xtype 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”具有 type forall t. (Maybe t, Maybe t)，其中两个组件都被强制为同一类型。这里x再次分配了 type Maybe t，带有tfresh，但不是泛化的。然后(x, x)被分配 type (Maybe t, Maybe t)。仅在顶层我们推广了加法forall t，但此时获得异构对为时已晚。

推荐阅读