OCaml：是否有类型为'a - >'的函数？ '除了身份识别功能？ [英] OCaml: Is there a function with type 'a -> 'a other than the identity function?

问题描述

顺便说一下，这不是一个家庭作业问题。它在课堂上长大了，但我的老师想不到。谢谢。

如果你只考虑语法，有不同的身份函数，它们都有正确的类型：

  let fx = x 
 let f2 x =（fun y  - > y）x 
 let f3 x =（fun y  - > y）（fun y  - > y）x 
 let f4 x = （fun y  - > y）y）x 
 let f5 x =（fun yz  - > z）xx 
 let f6 x = if false然后x else x 
  

还有更多的weirder函数：

  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 ，我们有 fx = x

这个方程不依赖于具体功能，它由类型唯一确定。有几个定理（框架在不同的上下文中）将形式化为多态函数不能改变多态类型的参数，只传递它的非正式思想。例如参见Philip Wadler的论文，定理免费！ a>。

这些定理的好处在于它们不仅适用于'a - > '一个的情况，这并不是那么有趣。你可以从（'a - >'a - > bool） - >中得到一个定理。 '列表 - > '一个列表类型的排序函数，它表示它的应用程序通过单调函数的映射进行通信。
更正式地说，如果你有这样一个类型的函数 s ，那么对于所有类型 u，v ，函数 cmp_u：u - > u - > bool ， cmp_v：v - > v - > bool ， f：u - >如果 cmp_u u u'意味着 code> cmp_v（fu）（f u'）（f是单调的），你有：

  map f（s cmp_u li）= s cmp_v（map f li）
  

这是当 s 完全是一个排序函数时的确如此，但我发现它能够证明它对任何函数 s


一旦你允许非终止，可以通过发散（无限循环，如> let rec fx = fx 函数），或者通过引发异常，当然你可以有任何东西：你可以构建一个类型为'a - >的函数。 'b ，类型并不代表任何事情。使用 Obj.magic：'a - > 'b 具有相同的效果。





有一些更为简单的方法可以失去与身份的对等：您可以在非空环境中工作，预定义的值可以从函数中访问。考虑下面的函数：

pre $ $ $ c $ let $ counter $ ref
let f x = incr counter; x


你仍然认为对于所有x， fx = x ：如果你只考虑返回值，你的函数仍然表现为身份。但是一旦你考虑到副作用，你就不再等同于（无副作用）身份：如果我知道 counter ，我可以写一个分离函数当给定此函数 f 时返回 true ，并且对于纯粹的身份函数返回false。

 让单独g = 
让before =！counter在
g（）; 
！counter = before + 1 
  

如果计数器被隐藏（例如通过模块签名，或简单地 let f = let counter = ... in fun x - > ... ），并且没有其他函数可以观察它，那么我们再次不能区分 f 和纯粹的身份函数。所以这个故事在当地州的存在下更加微妙。

This isn't a homework question, by the way. It got brought up in class but my teacher couldn't think of any. Thanks.

解决方案

How do you define the identity functions ? If you're only considering the syntax, there are different identity functions, which all have the correct type:

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

There are even weirder functions:

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

If you restrict yourself to a pure subset of OCaml (which rules out f7 and f8), all the functions you can build verify an observational equation that ensures, in a sense, that what they compute is the identity : for all value f : 'a -> 'a, we have that f x = x

This equation does not depend on the specific function, it is uniquely determined by the type. There are several theorems (framed in different contexts) that formalize the informal idea that "a polymorphic function can't change a parameter of polymorphic type, only pass it around". See for example the paper of Philip Wadler, Theorems for free!.

The nice thing with those theorems is that they don't only apply to the 'a -> 'a case, which is not so interesting. You can get a theorem out of the ('a -> 'a -> bool) -> 'a list -> 'a list type of a sorting function, which says that its application commutes with the mapping of a monotonous function. More formally, if you have any function s with such a type, then for all types u, v, functions cmp_u : u -> u -> bool, cmp_v : v -> v -> bool, f : u -> v, and list li : u list, and if cmp_u u u' implies cmp_v (f u) (f u') (f is monotonous), you have :

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

This is indeed true when s is exactly a sorting function, but I find it impressive to be able to prove that it is true of any function s with the same type.

Once you allow non-termination, either by diverging (looping indefinitely, as with the let rec f x = f x function given above), or by raising exceptions, of course you can have anything : you can build a function of type 'a -> 'b, and types don't mean anything anymore. Using Obj.magic : 'a -> 'b has the same effect.

There are saner ways to lose the equivalence to identity : you could work inside a non-empty environment, with predefined values accessible from the function. Consider for example the following function :

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

You still that the property that for all x, f x = x : if you only consider the return value, your function still behaves as the identity. But once you consider side-effects, you're not equivalent to the (side-effect-free) identity anymore : if I know counter, I can write a separating function that returns true when given this function f, and would return false for pure identity functions.

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

If counter is hidden (for example by a module signature, or simply let f = let counter = ... in fun x -> ...), and no other function can observe it, then we again can't distinguish f and the pure identity functions. So the story is much more subtle in presence of local state.

这篇关于OCaml：是否有类型为'a - >'的函数？ '除了身份识别功能？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！