将自身作为参数的函数的 Hindley-Milner 类型答案

【问题标题】：Hindley-Milner type of a function that takes itself as an argument将自身作为参数的函数的 Hindley-Milner 类型
【发布时间】：2019-12-28 05:42:01
【问题描述】：

假设你有一个函数 f，它的用法如下：

(f f (x-1))

你能推断出 f 的类型吗？

好像是递归的，即f :: (ftype) -> int -> int。

【问题讨论】：

对，我认为该表达式在当前的 Haskell 中不可能有效。
@Ry 为什么不呢？对我来说似乎有效。
@RobinZigmond 除非f 是多态的，并且编译器隐式添加了一些类型参数，否则您不能将f 应用于自身并具有要键入的表达式。你需要类似递归类型的东西来包装f，比如newtype。否则你会得到f :: T -> U 和f f 触发T ~ T -> U 被拒绝，因为在“发生检查”步骤中统一失败，因为它会产生无限类型。（同样，像f = id 这样的多态函数可以使f f 被键入，因为每个f 实际上是一个不同的实例化。）
@chi - 公平点，我认为出于某种原因我将表达式误读为 f (f (x - 1)) ，这当然是非常不同的。但即使如您自己指出的那样，它也适用于某些多态函数f，所以我仍然会质疑“该表达式在当前 Haskell 中（不可能）有效”的说法。

标签： haskell hindley-milner

【解决方案1】：

如果函数的参数是该函数本身，那么该类型必须是递归和无限的，这在 Haskell 中是非法的。然而，有一个漏洞：如果函数在那个参数中是多态的，那么它很好（尽管作为一个函数可能不是很有用）。有效f 的两个示例是id 和const id（对于它们中的任何一个，f f (x-1) 只会计算为x-1）。

【讨论】：

我认为“不是很有用”这一点可能值得商榷。例如，考虑(.) (.) 或fmap fmap。
@David Fair 点，但除非你有一个真的奇怪的 Num 实例在玩，我不认为任何这些更有用的功能会与 @987654329 进行类型检查@ 在他们之后。

【解决方案2】：

要回答这个问题，您可以应用类型推断算法。非正式地讨论它，您可以从声明f :: a -> b -> c 开始，因为它需要两个咖喱参数。你也可以推断出约束Num b，因为x - 1，所以f :: Num b => a -> b -> c。如果您知道x 是什么类型，可能会更多。但仅此而已。

例如，函数可以定义为f g x = undefined，在这种情况下，它的两个参数都被丢弃，并且返回类型不与任何输入类型统一。如果f 有一个函数体，那么你可以推断出更多。

【讨论】：

我不同意您关于 Num 约束的说法。现在，把f f 业务放在一边，假装你只是打电话给f (x-1)。现在，f 可能是 abs，它具有您声称的 Num 约束，或者它可能是 id，它根本没有约束，或者它可能是 take，它只接受一个 @ 987654336@.

【解决方案3】：

在您的标题中，您询问了f 的“Hindley-Milner 类型”。在通常的说法中，表达式的 HM 类型是通过应用于特定上下文的正式 HM 类型推断规则为表达式推断的主要（最一般）类型。因此，f 没有没有上下文的类型，并且表达式f f (x-1) 没有提供足够的上下文信息来键入f。上下文可以在“开始时”给出，也可以通过使用 lambda 或 let 表达式来开发。开发的上下文将确定是否可以为f 推断出 HM 类型，如果可以，该类型是什么。

例如较大的表达式：

let f = \y -> y in \x -> f f (x-1)

可以在空上下文中输入。如果- 运算符是Integer 减法，则无需详细介绍，它会推断f 的类型为forall a. a -> a 和整个表达式的Integer -> Integer 类型。（HM 类型系统没有类型类和约束的概念，例如 Num。）所以，这里，f 的 HM 类型是 forall a. a -> a，它在表达式 f f (x-1) 中的使用没有t 真的影响它的类型。这对于使用let 表达式引入f 的表达式很典型。例如较大的表达式：

let f = \y -> \z -> y in \x -> f f (x-1)

也很好打字。为f 推断的类型是forall a b. a -> b -> a（这是\y -> \z -> y 的明显类型，不受表达式其余部分的影响）。整个表达式的类型为forall a b. Integer -> a -> b -> a。

相比之下，如果f 是通过lambda 表达式引入的，那么情况就不同了，表达式f f (x-1) 确实会影响f 的推断类型。例如较大的表达式：

\f -> \x -> f f (x-1)

在 HM 中类型错误，因此不会为 f 或整个表达式推断类型。如果双 lambda 的主体发生变化，则可以根据表达式为 f 推断出不同的 HM 类型：

\f -> \x -> f (f x x) (x-1)   -- f :: Integer -> Integer -> Integer
\f -> \x -> f x + f x         -- f :: forall a. a -> Integer

Sooooo... 总而言之，仅从表达式 f f (x-1) 无法推断出 f 的类型，因为上下文不足。在 f 由 let 表达式引入的上下文中，f 的类型将严格从 f 的定义中推断出来，并且只要该类型与表达式 f f (x-1) 兼容，请键入推理会成功。相反，在 f 由 lambda 表达式引入的上下文中，表达式 f f (x-1) 类型错误，因此无法推断 f 的类型。

【讨论】：