bottom types and threaded exits

[Julian Assange <proff@iq.org>]

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, e.g:

let f a =
        try 
          f a
        with
          Failure _ -> exit(1)

How can one force 'a? For instance, Thread.exit and

        let f () = while true do () done 

has a type of unit -> unit.

One can write something such as

        let f () = while true do () done ; Pervasives.exit (1)

But this is clearly a hack.

If the type of Pervasices.exit is traced back, it originates in the
`external affairs powers' of the ocaml type system and is thus not
prone to type inferment. Functions never normally cause an *increase*
in generality. Trying to define a type of int -> 'a naturally leads
to a compiler error of 'a being unbound.

Cheers,
Julian.