OCaml:除了身份函数之外,是否存在类型为"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的论文,定理免费!.

这些定理的好处在于它们不仅适用于'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,和列表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,我可以写一个分离函数,true当给定这个函数时返回f,并且对于纯身份函数将返回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.

如果我们只允许全部功能,问题就会变得更有趣.不使用邪恶的技巧,不可能写出类型的总函数'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>