From mboxrd@z Thu Jan  1 00:00:00 1970
Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id VAA31940 for caml-red; Tue, 26 Sep 2000 21:16:20 +0200 (MET DST)
Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id UAA12864 for <caml-list@pauillac.inria.fr>; Mon, 25 Sep 2000 20:37:14 +0200 (MET DST)
Received: from isil.localdomain (ISIL.WV.CC.CMU.EDU [128.2.66.210])
	by nez-perce.inria.fr (8.10.0/8.10.0) with ESMTP id e8PIbD120474
	for <caml-list@inria.fr>; Mon, 25 Sep 2000 20:37:13 +0200 (MET DST)
Received: by isil.localdomain (Postfix, from userid 1000)
	id EED873745D; Mon, 25 Sep 2000 14:38:25 -0400 (EDT)
To: Remi VANICAT <remi.vanicat@labri.u-bordeaux.fr>
Cc: caml-list@inria.fr
Subject: Re: bottom types and threaded exits
References: <wx4s37qj6b.fsf@foo.iq.org>
	<ya3vgvkbx71.dlv@serveur1-1.labri.u-bordeaux.fr>
From: John Prevost <jmp@arsdigita.com>
Date: 25 Sep 2000 14:38:25 -0400
In-Reply-To: Remi VANICAT's message of "25 Sep 2000 12:08:50 +0200"
Message-ID: <87em28e2qm.fsf@localhost.localdomain.>
User-Agent: Gnus/5.0808 (Gnus v5.8.8) Emacs/20.7
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Sender: weis@pauillac.inria.fr

>>>>> "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.