## 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!