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 VAA26500 for caml-red; Tue, 26 Sep 2000 21:27:13 +0200 (MET DST) Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id LAA17725 for ; Tue, 26 Sep 2000 11:16:54 +0200 (MET DST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.10.0/8.10.0) with ESMTP id e8Q9Gd511476; Tue, 26 Sep 2000 11:16:39 +0200 (MET DST) Received: (from xleroy@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id LAA21722; Tue, 26 Sep 2000 11:16:39 +0200 (MET DST) Message-ID: <20000926111639.29744@pauillac.inria.fr> Date: Tue, 26 Sep 2000 11:16:39 +0200 From: Xavier Leroy To: Julian Assange , caml-list@inria.fr Subject: Re: bottom types and threaded exits References: Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Mailer: Mutt 0.89.1 In-Reply-To: ; from Julian Assange on Sun, Sep 24, 2000 at 01:25:48AM +1100 Sender: weis@pauillac.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