无限递归函数的推断类型答案

【问题标题】：Inferred type of an infinitely recursive function无限递归函数的推断类型
【发布时间】：2018-07-29 12:09:22
【问题描述】：

对于如下循环：

let rec loop () = loop ()

根据 try.ocamlpro.com 的签名是：

val loop : unit -> 'a = <fun>

为什么会这样？ loop() 永远不会停止调用自己，所以它不应该返回任何东西吗？

【问题讨论】：

除了好的答案之外，您可以考虑if x then 1 else loop ()是否应该产生类型错误。 if x then "string" else loop ()呢？

【解决方案1】：

是的，它应该，这正是unit -> 'a 的意思：给定调用者要求的任何类型'a，该函数承诺返回一个'a。

【讨论】：

我会有点不同（本着partial vs. complete correctness 的精神），该函数承诺如果成功返回，其结果将是类型'a.
更准确的说法是“给定一个unit，如果它成功返回，......”以反映调用者可以给出一个非终止表达式作为参数。
我认为在像 OCaml 这样的按值调用语言中，终止对参数的求值是调用者的问题，而不是被调用者的问题，但这真的很糟糕-主题。
@AlexeyRomanov：“给定一个单元，如果它返回成功，......”反映调用者必须先传递一个单元。它可能是一种不带参数的方法。 :) 或者只是将循环作为值传递而不调用它。

【解决方案2】：

我相信有人可以并且将会准确解释这是如何推断的，但它是 Hindley-Milner 类型系统及其推断算法的一个属性，它将能够推断出表达式的最一般类型.那当然是'a，它将与任何事物统一。

所以，凭直觉，如果您从最通用的类型'a 开始，然后尝试找到缩小范围的约束，在这种情况下您将找不到任何东西。唯一可以约束它的表达式是递归调用，我们已经假设它是'a，所以没有冲突。

【讨论】：