On 30 Sep 2000, Stefan Monnier wrote:

> A function of type "t1 -> t2" does not necessarily return an object of type t2.
> But if it does return, then the value is of type t2.
> Similarly, a function of type "t1 -> 'a" (if it returns) returns an value
> of type 'a.  Parametricity allows us to infer from that that if t1 does
> not contain 'a as a free type variable, then the function will necessarily
> never return (since it has no way to construct an value of
> type 'a).

This may be too obvious to point out, but that statement isn't always
true. From the Pervasives library:

  val input_value : in_channel -> 'a

clearly returns. I don't quite understood why the return type isn't
a monomorphic type variable though.

Patrick Doane