From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.7 required=5.0 tests=AWL,SPF_FAIL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 0FE4ABC69 for ; Mon, 30 Jul 2007 06:44:48 +0200 (CEST) Received: from ciao.gmane.org (main.gmane.org [80.91.229.2]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l6U4ijrt009177 (version=TLSv1/SSLv3 cipher=AES256-SHA bits=256 verify=NO) for ; Mon, 30 Jul 2007 06:44:47 +0200 Received: from list by ciao.gmane.org with local (Exim 4.43) id 1IFN7Y-0006d0-B7 for caml-list@inria.fr; Mon, 30 Jul 2007 06:44:40 +0200 Received: from c-76-99-60-61.hsd1.pa.comcast.net ([76.99.60.61]) by main.gmane.org with esmtp (Gmexim 0.1 (Debian)) id 1AlnuQ-0007hv-00 for ; Mon, 30 Jul 2007 06:44:40 +0200 Received: from geoffw by c-76-99-60-61.hsd1.pa.comcast.net with local (Gmexim 0.1 (Debian)) id 1AlnuQ-0007hv-00 for ; Mon, 30 Jul 2007 06:44:40 +0200 X-Injected-Via-Gmane: http://gmane.org/ To: caml-list@inria.fr From: Geoffrey Alan Washburn Subject: Re: Void type? Date: Mon, 30 Jul 2007 00:44:29 -0400 Message-ID: <46AD6CAD.7000500@cis.upenn.edu> References: <46AC748B.10200@lix.polytechnique.fr> <200707291216.34682.jon@ffconsultancy.com> <46AC7BB8.8050609@gmail.com> <20070729124340.GA18564@furbychan.cocan.org> <46AC8EEF.1040102@gmail.com> <20070729170216.GA8137@furbychan.cocan.org> <46ACF35F.5070102@lix.polytechnique.fr> Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 7bit X-Complaints-To: usenet@sea.gmane.org X-Gmane-NNTP-Posting-Host: c-76-99-60-61.hsd1.pa.comcast.net User-Agent: Thunderbird 2.0.0.6pre (X11/20070728) In-Reply-To: <46ACF35F.5070102@lix.polytechnique.fr> Sender: news X-Miltered: at concorde with ID 46AD6CBD.001 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; ocaml:01 ocaml:01 val:01 logics:01 type-safe:01 model:01 subtyping:01 subtypes:01 wrote:01 arnaud:01 abstract:01 upenn:01 exception:01 proofs:01 proofs:01 Arnaud Spiwack wrote: > Well, I don't really know why to use a void type in OCaml as well, thus > my answer may be quite abstract. But when I provide a new type, I give a > way to build it and a way to use it. In the case of the void type, there > is no way to build an element of that type, but there is a way to use > one such element : a void element can be used in place of any type. I think this is a slightly, or perhaps merely subtly, misleading characterization. A void type (0), not to be confused with "void" as used by C, Java, etc. is a type without any inhabitants. It is the the programming language equivalent of falsehood in logic. Dually, the unit type (1), called "unit" in OCaml, has a single inhabitant and is the programming language equivalent of truth in logic. It is important to distinguish between a void element and the reasoning principle provided by its elimination form. A term of type void cannot be used in place of any type, but its elimination form which can be realized as a function with the signature val elim_void : void -> 'a can be used to seemingly produce a value of any type. However, most realistic programming languages are not usable as consistent logics, and therefore have means to construct "proofs of falsehood", that is expressions with a void type. If you are using a type-safe language, unless you are subverting the type system, for example by using Obj.magic, all of these "proofs" are usually a diverging expression or one that makes use of some kind of control transfer such as an abort, invoking continuation, or raising an exception. So any implementation of elim_void will never actually return a value of any type. Elements of a "bottom" type more closely model something that may be used at any type. Bottom types show up more often in languages with subtyping, where they are subtypes of all types. The null value in Java, while not having an explicit type of its own (to my knowledge) is a good example of a bottom element. Hopefully this clarifies some confusion and conflation going on in this thread.