ocaml - 在OCaml中，这个: 'a. unit -> ' a是什么类型定义

Question

问题

这是我第一次看到像 'a. unit -> 'a 这样的类型定义。在 Explicit polymorphic type in record

第一季度 : 这是什么'a. (注意点)？

Q2 : 这种类型定义的术语是什么？

如果我做

let f:'a. 'a list -> int = fun l -> List.length l;;

乌托邦秀

val f : 'a list -> int = <fun>

Q3 : 为什么utop不显示类型 'a. 'a list -> int ?

Q4 : 我什么时候应该使用这种类型定义？

另外，我可以在记录中使用这种定义:

type t = { f: 'a. 'a list -> int};; (* this is correct *)

但我不能在变体中使用它:

type t = Node of ('a. 'a list -> int);; (* this is wrong *)

Q5 : 为什么？

更新/总结

我对此做了一些实验 forall type definition因为我在 OCaml 中找不到关于此主题的任何网络文章，我想归纳一下以找出背后的内容。

我在这里总结了这些实验，希望有人能提供更多的见解。

来自 answer下面和它的评论，我觉得 'a.是一种 force forall事物。

1. 'a.在函数定义中

let f:('a -> int) = fun x -> x + 1 (* correct *) 

以上很好，因为 OCaml 可以自由缩小 f 参数的类型并替换 'a与 int .

然而，

let f:'a. ('a -> int) = fun x -> x + 1 (* wrong *)

这不会通过编译器，因为它强制 f适用于 all types通过 '一种。 .显然，从定义部分看不可能是 x 唯一可能的类型。是 int .

这个例子很有趣，因为它展示了 OCaml 的静态类型推断系统背后的逻辑和魔法。类型通常从函数定义中自然地显示出来，即，您更关心函数的作用，而不是首先给出类型。

对我来说，真正使用 'a. 几乎没有意义。定义函数的时候，好像函数的定义可以处理所有类型，它的类型自然是 'a. ;如果函数无论如何都不能处理所有类型，那么强制所有类型是没有意义的。我想这就是为什么 OCaml 顶级通常不会打扰显示它的原因之一

2、'a.在类型推断中

let foo f = f [1;2;3] + f [4;5;6] (* correct *)

功能 f将被推断为 int list -> int因为 OCaml 看到 [1;2;3]首先是 int list ，所以 OCaml 假设 f将采取 int list .

这也是为什么下面的代码失败的原因，因为第二个列表是 string list

let foo f = f [1;2;3] + f ["1";"2";"3"] (* wrong*)

就算我知道 List.length将是 f 的不错选择, 由于类型推断系统，OCaml 将不允许。

我想如果我强制 f 是 'a. ，然后 f可以同时处理 int list和 string list在 foo ， 所以我做了:

let foo (f:'a. 'a list -> int) = f [1;2;3] + f ["1";"2";"3"];; (* wrong *)

它失败了，OCaml 似乎不允许。我想这就是为什么在存在不可预测的多态性的情况下不能总是进行类型推断的原因，所以 OCaml 将其使用限制为记录字段和对象方法。

3. 'a.记录中

通常我拿 'a从这样的类型参数:

type 'a a_record = {f: 'a list -> int};; (* correct *)

但是，限制是一旦你申请，你就会得到具体的类型:

let foo t = t.f [1;2;3] + t.f [4;5;6];;  (* correct *)

OCaml 将推断 t作为 int a_record ，不是 'a a_record了。所以下面会失败:

let foo t = t.f [1;2;3] + t.f ["1";"2";"3"];; (* wrong*)

在这种情况下，我们可以使用 'a.因为 OCaml 允许它在记录类型中。

type b_record = {f: 'a. 'a list -> int};; (* correct *)
let foo t = t.f [1;2;3] + t.f ["1";"2";"3"];; (* correct *)

b_record本身是一个具体的记录类型，它的 f可以应用于所有类型的列表。那么我们的 foo以上将通过OCaml。

Answer 1

'a.意思是“对于所有类型'a”。 OCaml 顶层通常不会显示它，这就是它没有出现在输出中的原因。除非在其他地方显示，否则任何打印的包含类型变量的表达式在开头都有一个隐式的 forall。

在定义函数时，在开始时添加它以确保类型是多态的会很有用。例如

# let f : ('a -> 'a) = fun x -> x + 1;;
val f : int -> int = <fun>

在这里， 'a -> 'a只是将函数的输出类型限制为与其输入类型相同，但 OCaml 可以自由地进一步限制它。与 'a. ，这不会发生:

# let f : 'a. ('a -> 'a) = fun x -> x + 1;;
Error: This definition has type int -> int which is less general than
     'a. 'a -> 'a

您需要指定 'a.当定义记录或对象类型并且您希望将类型变量范围限定为单个成员而不是整个对象时。