functional-programming - `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（它具有用于表述这种类型的指示性多态性）。