在OCaml中,这是什么类型的定义:'a.单位 - >'a

Question

问题

这是我第一次见到型定义,就像'a. unit -> 'a在创纪录的显性多态类型

Q1:这是什么'a.(注意点)？

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

---

如果我做

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

utop显示

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中这个主题的任何文章,我想引导找出背后的内容.

我在这里总结了这些实验,并希望有人可以提供更多见解.

---

从下面的答案和它的评论,我觉得'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]首先看到并且它是a 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似乎不允许它.我想这就是为什么你不能总是在存在impredicative多态的情况下进行类型推断,因此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.意思是"适用于所有类型".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.何时定义记录或对象类型,并且您希望将类型变量的范围限定为单个成员而不是整个对象.