where 子句中的类型推断

Question

如果我写

foo :: [Int]
foo = iterate (\x -> _) 0

GHC 高兴地告诉我那x是一个Int，那个洞应该是另一个Int。但是，如果我将其重写为

foo' :: [Int]
foo' = iterate next 0
  where next x = _

它不知道 的类型x，也不知道洞是什么。如果我使用let.

where除了手动添加类型签名之外，还有什么方法可以恢复绑定中的类型推断？

Answer 1

并不真地。这种行为是设计使然，继承自理论上的 Hindley-Milner 类型系统，该系统形成了 Haskell 类型系统的最初灵感。（这种行为被称为“let-多态性”，可以说是 HM 系统最关键的特征。）

粗略地说，lambda 的类型是“自上而下”的：在对包含的表达式进行类型检查时（具体来说，在对 的参数进行类型检查时），(\x -> _)首先为表达式分配类型，然后使用该类型来推断和 的类型的洞。Int -> Intiteratex :: Int_ :: Int

相反，let和where绑定变量是“自下而上”类型的。首先推断的类型next x = _，与它在主表达式中的使用无关，一旦确定了该类型，就会根据它在表达式 中的使用情况进行检查iterate next 0。在这种情况下，表达式next x = _被推断为具有相当无用的类型p -> t。iterate next 0然后，根据其在专门用于Int -> Int（通过采用p ~ Int和）的表达式中的使用来检查该类型t ~ Int并成功进行类型检查。

在没有这种区别（并忽略递归绑定）的语言/类型系统中，子句where只是 lambda 绑定和应用程序的语法糖：

foo = expr1 where baz = bazdefn   ==>   foo = (\baz -> expr1) bazdefn

因此，您可以做的一件事是将子句“脱糖”where为“等效”lambda 绑定：

foo' :: [Int]
foo' = (\next -> iterate next 0) (\x -> _)

当然，这种语法在物理上是令人排斥的，但它确实有效。由于 lambda 是自上而下的类型，因此x和hole 的类型都为Int。