Re: bottom types and threaded exits

[John Prevost <jmp@arsdigita.com>]

>>>>> "rv" == Remi VANICAT <remi.vanicat@labri.u-bordeaux.fr> writes:

    rv> Julian Assange <proff@iq.org> writes:
    >> 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.

>From what I can tell, what you're trying to do here is just make the
result type of a non-terminating computation go to 'a.  This is
actually quite easy--you just need to loop in a way that doesn't
constrain the type.  while ... do ... done always returns unit (which
is good, since usually you use it in a way that terminates.

The appropriate way to do it that will get type 'a is (in your case):

let rec f () = f ()

Note that if you choose the more direct translation

let rec f () = if true then f ()

you get constrained to type unit -> unit again, since a one-branched
if returns unit for the else branch.

So, an example of a vaguely useful function would be:

let rec call_forever f x = f x; call_forever f x

which has type:

val call_forever : ('a -> 'b) -> 'a -> 'c


So, it is not so much that 'a as bottom is a hack, as that the system
only produces such types when the result type is totally
unconstrained--and that doesn't happen with things like while loops,
only with recursion--where a function always returns the result of
calling itself (or another such function.)


John.