OCaml:除了identity函数之外，还有其他类型为'a ->‘的函数吗？

Question

顺便说一句，这不是一个家庭作业问题。它是在课堂上被提出来的，但我的老师想不出任何一个。谢谢。

Answer 1

如何定义标识函数？如果你只考虑语法，有不同的标识函数，它们都有正确的类型：

let f x = x
let f2 x = (fun y -> y) x
let f3 x = (fun y -> y) (fun y -> y) x
let f4 x = (fun y -> (fun y -> y) y) x
let f5 x = (fun y z -> z) x x
let f6 x = if false then x else x

还有更奇怪的函数：

let f7 x = if Random.bool() then x else x
let f8 x = if Sys.argv < 5 then x else x

如果您将自己限制为OCaml的一个纯子集(它排除了f7和f8)，那么您可以构建的所有函数都会验证一个观察方程，该方程在某种意义上确保它们计算的是同一性:对于所有值f : 'a -> 'a，我们都有那个f x = x

这个方程不依赖于特定的函数，它由类型唯一确定。有几个定理(在不同的上下文中)形式化了“多态函数不能改变多态类型的参数，只能传递它”这一非正式的想法。例如，请参阅Philip Wadler，Theorems for free!的论文。

这些定理的好处是它们不仅适用于'a -> 'a的情况，这并不是很有趣。你可以从排序函数的('a -> 'a -> bool) -> 'a list -> 'a list类型中得到一个定理，即它的应用程序与一个单调函数的映射交换。更正式地说，如果您有任何具有这种类型的函数s，那么对于所有类型的u, v、函数cmp_u : u -> u -> bool、cmp_v : v -> v -> bool、f : u -> v和list li : u list，如果cmp_u u u'暗示cmp_v (f u) (f u') (f是单调的)，那么您将拥有：

map f (s cmp_u li) = s cmp_v (map f li)

当s确实是一个排序函数时，这确实是正确的，但我发现能够证明任何具有相同类型的函数s都是如此，这是令人印象深刻的。

一旦您允许非终止性，无论是通过发散(无限期循环，就像上面给出的let rec f x = f x函数一样)，还是通过引发异常，您当然可以拥有任何东西:您可以构建类型为'a -> 'b的函数，并且类型不再有任何意义。使用Obj.magic : 'a -> 'b也有同样的效果。

有更明智的方法来失去与标识的等价性:您可以在非空环境中工作，使用可从函数访问的预定义的值。例如，考虑以下函数：

let counter = ref 0
let f x = incr counter; x

你仍然认为对于所有x，f x = x：如果你只考虑返回值，你的函数仍然表现为标识。但是一旦你考虑到副作用，你就不再等同于(无副作用)标识:如果我知道counter，我可以编写一个单独的函数，当这个函数为f时，它返回true，而对于纯标识函数，将返回false。

let separate g =
  let before = !counter in
  g ();
  !counter = before + 1

如果计数器是隐藏的(例如，通过模块签名，或者仅仅是let f = let counter = ... in fun x -> ...)，并且没有其他函数可以观察到它，那么我们同样不能区分f和纯标识函数。因此，在存在局部状态的情况下，故事要微妙得多。

Answer 2

let rec f x = f (f x)

这个函数永远不会终止，但它的类型是'a -> 'a。

如果我们只允许使用total函数，这个问题就会变得更加有趣。如果不使用邪恶的技巧，就不可能编写'a -> 'a类型的全函数，但是邪恶的技巧很有趣，所以：

let f (x:'a):'a = Obj.magic 42

Obj.magic是一种令人讨厌的'a -> 'b类型，它允许各种恶作剧绕过类型系统。

转念一想，它也不是完全的，因为它在与盒装类型一起使用时会崩溃。

所以真正的答案是:恒等函数是唯一的'a -> 'a类型的全函数。

Answer 3

抛出异常也会给你一个'a -> 'a类型：

# let f (x:'a) : 'a = raise (Failure "aaa");;
val f : 'a -> 'a = <fun>