GHC/GHCi意外接受的代码

Question

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

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

由于每个组件都绑定到同一变量x，所以我期望这个表达式的最一般类型为(Maybe a, Maybe a)。如果我使用where而不是let也会得到相同的结果。我有什么遗漏吗？

- tlon

---

猜测：这是let多态性。我们预计单态限制将适用，但仅在存在类约束时才会发生，以避免计算重复（因为约束在幕后成为函数）。如果您提供签名(Maybe Int, Maybe Double)并使用x = Just 0，则确实会出现错误，这证实了这个故事（请记住，数字文字是多态的）。 - luqui

@luqui 我尝试了 let { foo :: (Maybe Int, Maybe Double) ; foo = let {x=Just 0} in (x,x) }，它可以正常工作，没有出现任何错误。 (?) 这甚至可以与 foo :: (Integral a, Fractional b) => (Maybe a, Maybe b) 一起使用。 - Will Ness

Answer 1

简单来说，使用 let 可以推广 x 的类型。这是 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 的类型 "仅" 为 forall t. (Maybe t, Maybe t)，其中两个组件被强制为相同的类型。这里 x 再次分配为类型 Maybe t，其中 t 是新的，但它没有被推广。然后，(x, x) 被分配为类型 (Maybe t, Maybe t)。仅在顶层我们添加 forall t 进行泛化，但此时已经太晚了，无法获得异构对。

- chi

---

值得注意的是，启用某些 GHC 扩展会隐式禁用 let 泛化，即 GADTs 或 TypeFamilies。 - Alexis King

@AlexisKing，我无法验证。无论那些扩展名如何，该OP给出的示例都可以编译。你有例子吗？ - luqui

@AlexisKing 在这里不适用。MonoLocalBinds 只适用于那些具有自由变量的绑定组，它们受单态限制影响或既不是 let-bound 也不是顶层的。作为数据构造函数的 Nothing 同时既未被单态化也是顶层的，因此绑定组 x = Nothing 可以被恰当地泛化。 - HTNW

@luqui：奇怪了；GHC文档说MonoLocalBinds被TypeFamilies和GADTs隐含，没有其他扩展。编辑：啊，这是真的，但与此特定示例无关。 - Jon Purdy

@HTNW 是的，你说得对，但是这个答案更普遍地讲述了let泛化，并没有提到在GHC Haskell中let只有有时被泛化。 - Alexis King