From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 13DD4BC51 for ; Mon, 29 Nov 2004 01:02:11 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id iAT02Al8011072 for ; Mon, 29 Nov 2004 01:02:10 +0100 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 BAA03312 for ; Mon, 29 Nov 2004 01:02:10 +0100 (MET) Received: from kurims.kurims.kyoto-u.ac.jp (kurims.kurims.kyoto-u.ac.jp [130.54.16.1]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id iAT027GT029202 for ; Mon, 29 Nov 2004 01:02:09 +0100 Received: from localhost (suiren [130.54.16.25]) by kurims.kurims.kyoto-u.ac.jp (8.13.1/8.13.1) with ESMTP id iAT024VJ020960; Mon, 29 Nov 2004 09:02:06 +0900 (JST) Date: Mon, 29 Nov 2004 09:01:51 +0900 (JST) Message-Id: <20041129.090151.110958815.garrigue@math.nagoya-u.ac.jp> To: tews@tcs.inf.tu-dresden.de Cc: caml-list@inria.fr Subject: Re: [Caml-list] Why doesn't ocamlopt detect a missing ; after failwith statement? From: Jacques Garrigue In-Reply-To: References: <1101438486.9291.138.camel@pelican.wigram> <20041126.142525.93385094.garrigue@math.nagoya-u.ac.jp> X-Mailer: Mew version 4.0.64 on Emacs 21.3 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Miltered: at nez-perce with ID 41AA6702.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 41AA66FF.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 ocamlopt:01 failwith:01 hendrik:01 tews:01 tews:01 pointers:01 semantics:01 forall:01 pointer:01 pointer:01 model:01 ...:98 ...:98 writes:01 X-Spam-Checker-Version: SpamAssassin 3.0.0 (2004-09-13) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.0 X-Spam-Level: From: Hendrik Tews > Jacques Garrigue writes: > > Note that void in C is definitely not zero. You cannot have variables > > C++ standard, 3.9.1.9: The void type has an empty set of values. ... > > So I would say void is zero. On the other side you have functions > returning void. Therefore I would conclude that the type theory > of C++ is unsound. Which is almost the same thing as saying that the definition contradicts itself... My point was just that, looking at the way void is used in C, it clearly does not have the usual proporties of zero, and among them the fact no function should be able to return zero, or that all pointers to void should be NULL. For this reason it seems to me at first that the actual semantics of void in C is that of (\exists a. a) aka unit (i.e. a value we know nothing about), not that of (\forall a.a) aka zero (the impossibility). You can safely cast any pointer to a void pointer, but not the opposite. Additionaly, for representation reasons, you cannot copy or allocate values of type void, so that they are non-existent in practice, but this looks more like a consequence than a definition. Another meaning of void seems to be the empty product, which again is unit, with the extract constraint that you cannot store such a value in C. This is just my personal take on the question. I just don't think that there is any serious model theory behind C's void, just a bunch of practical constraints. Jacques Garrigue