Polymorphism and return values of functions
Objective CAML's parametric polymorphism permits the definition of
functions whose return type is completely unspecified. For example:
# let id x = x ;;
val id : 'a -> 'a = <fun>
However, the return type depends on the type of the argument. Thus, when
the function id is applied to an argument, the type inference
mechanism knows how to instantiate the type variable 'a. So for
each particular use, the type of id can be determined.
If this were not so, it would no longer make sense to use strong static
typing, entrusted with ensuring execution safety. Indeed, a function of
completely unspecified type such as 'a -> 'b would allow any type
conversion whatsoever, which would inevitably lead to a run-time error
since the physical representations of values of different types are not the
same.
Apparent contradiction
However, it is possible in the Objective CAML language to define a function whose
return type contains a type variable which does not appear in the types of
its arguments. We will consider several such examples and see why such a
possibility is not contradictory to strong static typing.
Here is a first example:
# let f x = [] ;;
val f : 'a -> 'b list = <fun>
This function lets us construct a polymorphic value from anything at all:
# f () ;;
- : '_a list = []
# f "anything at all" ;;
- : '_a list = []
Nevertheless, the value obtained isn't entirely unspecified: we're dealing
with a list. So it can't be used just anywhere.
Here are three examples whose type is the dreaded 'a -> 'b:
# let rec f1 x = f1 x ;;
val f1 : 'a -> 'b = <fun>
# let f2 x = failwith "anything at all" ;;
val f2 : 'a -> 'b = <fun>
# let f3 x = List.hd [] ;;
val f3 : 'a -> 'b = <fun>
These functions are not, in fact, dangerous vis-a-vis execution safety,
since it isn't possible to use them to construct a value: the first one loops forever, the
latter two raise an exception which interrupts the computation.
Similarly, it is in order to prevent functions of type
'a -> 'b from being defined that new exception constructors are
forbidden from having arguments whose type contains a variable.
Indeed, if one could declare a polymorphic exception
Poly_exn of type 'a -> exn, one could then write the
function:
let f = function
0 -> raise (Poly_exn false)
| n -> n+1 ;;
The function f being of type int -> int and
Poly_exn being of type 'a -> exn, one could then define:
let g n = try f n with Poly_exn x -> x+1 ;;
This function is equally well-typed (since the argument of
Poly_exn may be arbitrary) and now, evaluation of (g 0)
would end up in an attempt to add an integer and a boolean!