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 OAA24211 for caml-red; Sat, 30 Sep 2000 14:55:09 +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 LAA21810 for ; Sat, 30 Sep 2000 11:13:09 +0200 (MET DST) Received: from suburbia.net (suburbia.net [203.4.184.1]) by concorde.inria.fr (8.10.0/8.10.0) with ESMTP id e8U9D4n21468; Sat, 30 Sep 2000 11:13:05 +0200 (MET DST) Received: by suburbia.net (Postfix, from userid 110) id 4DDF66C4D4; Sat, 30 Sep 2000 20:12:52 +1100 (EST) To: Xavier Leroy Cc: caml-list@inria.fr Subject: Re: bottom types and threaded exits References: <20000926111639.29744@pauillac.inria.fr> Cc: proff@iq.org From: Julian Assange Date: 30 Sep 2000 20:12:52 +1100 In-Reply-To: Xavier Leroy's message of "Tue, 26 Sep 2000 11:16:39 +0200" Message-ID: User-Agent: Gnus/5.0802 (Gnus v5.8.2) XEmacs/21.1 (Big Bend) MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Sender: weis@pauillac.inria.fr Xavier Leroy writes: > 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. Yes, I found that quite cool. > 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. It depends on what level of semantics you are looking at. As far as type proofing is concerned, 'a is correct. However at a higher level you can say `the function never returns so saying that it returns any type is incorrect'. The problem is that some functions that do return, return 'a. Ocaml's overloading of 'a, is much the same as lisps overloading of nil and C's overloading of 0 or void*. You might counter saying that 'a is defined in terms of type-unification, thus reading additional meaning into the type is bogus. But such a view denies the semantics of what is being typed. A computer language -- one of the important semantics of which is that is capable of capable of generating functions that fail to return. > 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. I've used: let exit = Thread.exit (); assert false to get the required type. While clearly a hack, it's better to use a simple construct like this instead of having a casting to 'a mechanism. Although I find full-bown determinacy types, mercury style (but god forbid mercury heavy handed type syntax) quite appealing. > 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. This is fair. I think an assert false at the end of the loop, or let bottom f = f (); assert false bottom (fun () -> while true do () done) is effective. Although, once again, it'd be nice to see a 'bottom rather than 'a type come out of this, even if the two are semantically equivalent in the eye of the type checker. Cheers, Julian.