Previous Contents Next

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!

Previous Contents Next