使用 -rectypes 有哪些权衡？

Question

我问了一个问题，为什么我尝试进行函数链接不起作用：使函数在完成一些工作后返回自身，答案是：要使函数返回自身，您需要启用递归类型-rectypes。这让我很困惑。为什么这个功能隐藏在编译器标志后面？必须有充分的理由不默认启用它。所以我的问题是：使用这个标志时有什么权衡？我应该避免它，还是可以安全地将它用于我的所有代码，并且它不是仅与旧代码兼容？

Answer 1

简而言之，递归类型对于许多用户来说既令人困惑，又对于可能需要它们的专家用户来说通常是可以避免的。这就是为什么该-rectypes选项自 OCaml 2.03 中引入以来从未成为默认选项。

\n

就错误而言，例如，考虑该append函数的错误实现

\n

let rec quasi_append l r = match l, r with\n| [], r -> r\n| l, [] -> l\n| x :: l, r -> x @ quasi_append l r  \n

\n

没有-rectypes类型系统会捕获错误：

\n

Error: This expression has type \'a list list\n       but an expression was expected of type \'a list\n       The type variable \'a occurs inside \'a list\n

\n

但是，-rectypes启用后，quasi_append\ntype 是一个有效函数val quasi_append : (\'a list as \'a) list -> \'a list -> \'a list，仅适用于...列表...空列表列表：

\n

quasi_append [[];[[[]]]; [[[[]]]] ] [[]] ===  [[[]]; [[[]]]; []]\n

\n

因此，-rectypes即使在初学者编写的代码中也引入了复杂类型（在前面的示例中，错误是单个::替换为@）。

\n

此外，即使对于专家用户来说，通常也可以避免显式递归类型。例如，您上一个问题中的函数可以通过添加一个递归类型定义而无需递归类型来编写

\n

Error: This expression has type \'a list list\n       but an expression was expected of type \'a list\n       The type variable \'a occurs inside \'a list\n

\n

fix在这里，我们使用递归代数类型这一事实来隐藏Fix构造函数后面的递归。\n然后，我们只需将 log 函数装箱在Fix构造函数中\n即可避免出现显式递归类型：

\n

let rec log x = Printf.printf "%d" x; Fix log\n

\n

我们甚至可以定义一个辅助应用程序运算符，在为我们应用之前取消函数的装箱\n

\n

let ($) (Fix f) x = f x\n

\n

最后，我们可以log通过$在每个应用程序之间插入来使用

\n

let boxed_log = log 111 $ 222 $ 333 $ 444 \n

\n

使用这些技术，专家用户通常可以避免递归类型。\n此外，有一个需要使用的例外-rectypes：递归对象和多态变体。递归对象和多态变体通常都需要递归类型，但很容易识别涉及其中任何一个的代码。因此，对于多态变体类型和对象类型，默认启用递归类型。例如，可以编写一个带有log返回整个对象的方法的对象

\n

quasi_append [[];[[[]]]; [[[[]]]] ] [[]] ===  [[[]]; [[[]]]; []]\n

\n

o那么的类型是< log : int -> \'a > as \'a。

\n

因此，选择留给-rectypes专家用户，他们确信他们需要增加复杂性（例如，证明助手Coq所依赖的）。-rectypes

\n\n

\xc2\xb9 未装箱的注释告诉编译器，它可以将函数直接存储在内存中，\n因为只有一个构造函数。\n因此类型构造函数仅在类型检查时存在。

\n