`fun x - > x`是OCaml中唯一具有'a - >'a类型的函数吗？

Question

标题是问题,简单.

身份功能fun x -> x具有类型'a -> 'a.

还有其他相同类型的功能'a -> 'a吗？

我想不出另一个.

Answer 1

没有.

fun x -> print_endline "foo"; x;;

(failwith "bang" : 'a -> 'a);;

(fun x -> failwith "bang" : 'a -> 'a);;

(fun x -> List.hd [] : 'a -> 'a);;

let rec f (x : 'a) : 'a = f x;;

let counter = ref 0;;
(fun x -> incr counter; x);;

身份功能是'a -> 'a总编程语言中唯一没有任何副作用的居民,包括不确定.OCaml和Haskell都没有资格,但是一些语言用作证明助手(这个总体很重要),特别是Coq(具有用于制定这种类型的不可预测的多态性).