关于OCaml -rectypes选项下递归类型推导的疑问

咱们一步步来捋清楚你遇到的这几个问题，都是和递归类型（-rectypes选项开启后允许的特性）以及类型系统里的发散表达式有关的~

1. fun x -> x x的类型推导 #

先看你贴的这个表达式：

# fun x -> x x;;
- : ('a -> 'b as 'a) -> 'b = <fun>

这个类型('a -> 'b as 'a) -> 'b怎么来的？咱们拆解一下：

• 假设参数x的类型是'a，那x x是把x当成函数来调用，参数也是x，所以x必须同时满足：它是一个函数，参数类型是自己的类型'a，返回类型是'b。
• 换句话说，'a的定义就是'a -> 'b，OCaml里用as关键字来表达这种递归类型绑定——'a -> 'b as 'a就是“'a是一个接受'a类型参数、返回'b类型的函数”。
• 整个匿名函数接受一个'a类型的参数（也就是这个递归函数类型），返回'b，所以最终类型就是('a -> 'b as 'a) -> 'b。

2. (fun x -> x x) (fun x -> x x)的类型与运行时行为 #

首先明确：这个表达式在类型层面是可推导的，但它的求值会陷入无限循环，这是两个不同的层面。

从类型推导来看：

• 我们已经知道fun x -> x x的类型是T = ('a -> 'b as 'a) -> 'b。
• 现在把一个T类型的函数作为参数传给另一个T类型的函数，那参数类型需要匹配：也就是T要等于'a（因为第一个fun x->x x的参数类型是'a）。
• 代入T的定义，就得到('a -> 'b as 'a) -> 'b = 'a，而'a本身又是'a -> 'b，所以展开后会变成无限递归的类型：((((...) -> 'b) -> 'b) -> 'b) -> 'b……
• 因为开启了-rectypes，OCaml允许这种无限递归的类型存在，所以类型检查是能通过的，但这个类型没有具体的有限表示形式。

而运行时无限循环的原因很直观：这个表达式相当于把自己传给自己，调用时会不断触发x x的调用，永远不会终止，所以你运行它的时候OCaml会一直循环下去。

3. fun _ -> (fun x -> x x) (fun x -> x x)的'a -> 'b类型解释 #

这个看起来有点反直觉，但其实是类型系统里的一个特性：发散表达式（永远不会终止的表达式）属于所有类型。

咱们拆解：

• 这个匿名函数接受任意类型的参数（'a），返回的是后面那个无限循环的表达式的结果。
• 因为后面的表达式永远不会返回（无限递归），它的类型是“bottom type”（⊥）——在类型理论里，⊥是所有类型的子类型，也就是说，⊥可以被当成任何类型'b来使用。
• 所以整个函数的类型就是'a -> 'b：不管你传什么类型的参数进去，函数返回的是一个可以适配任何类型的值（因为它永远不会返回，所以不会有类型不匹配的问题）。

内容的提问来源于stack exchange，提问作者vonaka