Hindley-Milner类型的函数，它将自身作为参数

Question

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

(f f (x-1)) 

关于f的类型，你能推断出什么？

它似乎是递归的，即f :：(ftype) int int -> ->。

Answer 1

如果函数的参数就是函数本身，那么类型必须是递归的和无限的，这在Haskell中是非法的。然而，有一个漏洞:如果函数在该参数中是多态的，那么它就没有问题(尽管作为函数可能不是很有用)。有效f的两个示例是id和const id (使用这两个示例中的任何一个，f f (x-1)的计算结果都将为x-1)。

Answer 2

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

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

Answer 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)

可以在空上下文中键入。在不了解细节的情况下，它会推断出f的类型forall a. a -> a和整个表达式的类型Integer -> Integer，前提是-运算符是Integer减法。( HM类型系统不像Num那样具有类型类和约束的概念。)因此，在这里，f的HM类型是forall a. a -> a，在表达式f f (x-1)中使用它并不会真正影响它的类型。这对于使用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是通过λ表达式引入的，那么事情就不同了，表达式f f (x-1)确实会影响f的推断类型。例如，较大的表达式：

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

在HM中类型错误，因此不能推断f的类型或整个表达式的类型。如果更改了双λ的主体，则可以根据表达式推断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

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