Filter
Top Products
2.6. EQUALITY OF FUNCTIONS 17
expression. However it may sometimes be convenient to restrict the generality of
a type. This cannot make code work that didn’t work before, but it may serve as
documentation regarding the intended purpose of the code; it is also possible to
use shorter synonyms for complicated types. Type restriction can be achieved in
CAML by adding type annotations after some expression(s). These type annotations
consist of a colon followed by a type. It usually doesn’t matter exactly where
these annotations are added, provided they enforce the appropriate constraints.
For example, here are some alternative ways of constraining the identity function
to type int -> int:
#let I (x:int) = x;;
I : int -> int = <fun>
#let I x = (x:int);;
I : int -> int = <fun>
#let (I:int->int) = fun x -> x;;
I : int -> int = <fun>
#let I = fun (x:int) -> x;;
I : int -> int = <fun>
#let I = ((fun x -> x):int->int);;
I : int -> int = <fun>
2.6 Equality of functions
Instead of comparing the actions of I and I
on particular arguments like 3, it
would seem that we can settle the matter definitively by comparing the functions
themselves. However this doesn’t work:
#I’ = I;;
Uncaught exception: Invalid_argument "equal: functional value"
It is in general forbidden to compare functions for equality, though a few special
instances, where the functions are obviously the same, yield true:
#let f x = x + 1;;
f : int -> int = <fun>
#let g x = x + 1;;
g : int -> int = <fun>
#f = f;;
it : bool = true
#f = g;;
Uncaught exception: Invalid_argument "equal: functional value"
#let h = g;;
h : int -> int = <fun>
#h = f;;
Uncaught exception: Invalid_argument "equal: functional value"
#h = g;;
it : bool = true
Why these restrictions? Aren’t functions supposed to be first-class objects in
CAML? Yes, but unfortunately, (extensional) function equality is not computable.
This follows from a number of classic theorems in recursion theory, such as the
unsolvability of the halting problem and Rice’s theorem.
7
Let us give a concrete
7
Rice’s theorem is an extremely strong undecidability result which asserts that any nontrivial
property of the function corresponding to a program is uncomputable from its text. An excellent
computation theory textbook is Davis, Sigal, and Weyuker (1994).