haskell - 在 where 子句中进行类型推断

Question

如果我写

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

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

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

它不知道 x 的类型是什么，也不是那个洞。如果我使用 let 也会发生同样的情况.
有没有办法恢复 where 中的类型推断？绑定(bind)，而不是手动添加类型签名？

Answer 1

并不真地。这种行为是设计使然，并且继承自形成 Haskell 类型系统最初灵感的理论 Hindley-Milner 类型系统。 (这种行为被称为“let-polymorphhism”，可以说是 H-M 系统最关键的特征。)
粗略地说，lambda 是“自上而下”键入的:表达式 (\x -> _)首先分配类型 Int -> Int在对包含表达式进行类型检查时(特别是在对 iterate 的参数进行类型检查时)，然后使用此类型推断 x :: Int 的类型和洞的_ :: Int .
相比之下，let和 where绑定(bind)变量是“自下而上”键入的。 next x = _的类型首先推断出来，与它在主表达式中的使用无关，一旦确定了该类型，就会检查它在表达式 iterate next 0 中的使用情况。 .在这种情况下，表达式 next x = _被推断具有相当无用的类型p -> t .然后，检查该类型在表达式 iterate next 0 中的使用情况。它专门用于Int -> Int (通过使用 p ~ Int 和 t ~ Int )并成功进行类型检查。
在没有这种区别的语言/类型系统中(并且忽略递归绑定(bind))，where子句只是 lambda 绑定(bind)和应用程序的语法糖:

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

所以你可以做的一件事是“脱糖”where “等效” lambda 绑定(bind)的子句:

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

当然，这种语法在物理上是令人厌恶的，但它确实有效。由于 lambda 的自上而下类型，x并且孔的类型为 Int .