Re: bottom types and threaded exits

[Xavier Leroy <Xavier.Leroy@inria.fr>]

> Pervasives.exit is of type int -> 'a
> Here we see ocaml using 'a to represent _|_. This hack is presumably
> so type unification still works in the face of potentially
> non-terminating computations

That's one way of putting it, but as Pierre Weis mentioned, fully
polymorphic types such as 'a appear naturally during type inference
for non-terminating expressions.

The prime example is recursive functions with no bottom case (let rec
f x = f (x + 1)), but raising an exception (raise Exn) also has type 'a.

Semantically, it is correct to assign type 'a to any expression that
never returns normally: there are no values of type 'a, but such
expressions never result in a value.

By the same reasoning, since a call to Pervasives.exit never returns,
it is safe and indeed logical to give it type int -> 'a.

Thread.exit should also have type unit -> 'a; the reason it currently
has type unit -> unit is due to the way it is implemented
(as Thread.kill(Thread.self())), but this is more of an historical
accident.

Finally, concerning "while true do e done", there is only one typing
rule in the type-checker for "while p do e done", which assumes that
"p" may become false and the loop may thus terminate with the result
"()", hence the "unit" type.

It would be semantically sound to give "while true do e done" the type
'a, but it would require a special type-checking rule for the "while"
construct when the predicate is "true", which sounds a bit weird.
However, we already implemented such a special case for "assert false"
(type 'a) w.r.t.  "assert cond" (type unit).

- Xavier Leroy