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.0 required=5.0 tests=AWL 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 DC35CBC69 for ; Mon, 30 Jul 2007 15:11:05 +0200 (CEST) Received: from smtp.janestcapital.com (www.janestcapital.com [66.155.124.107]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l6UDB4kq000704 for ; Mon, 30 Jul 2007 15:11:05 +0200 Received: from [172.25.129.161] [38.96.172.125] by janestcapital.com with ESMTP (SMTPD-9.10) id A37E0240; Mon, 30 Jul 2007 09:11:26 -0400 Message-ID: <46ADE367.8020801@janestcapital.com> Date: Mon, 30 Jul 2007 09:11:03 -0400 From: Brian Hurt User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.7.2) Gecko/20040804 Netscape/7.2 (ax) X-Accept-Language: en-us, en MIME-Version: 1.0 To: Geoffrey Alan Washburn Cc: caml-list@inria.fr Subject: Re: [Caml-list] Re: Void type? 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> <46AD6CAD.7000500@cis.upenn.edu> In-Reply-To: <46AD6CAD.7000500@cis.upenn.edu> Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 7bit X-Miltered: at concorde with ID 46ADE368.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; ocaml:01 ocaml:01 val:01 theorems:01 unify:01 wrote:01 wrote:01 arnaud:01 abstract:01 exception:01 caml-list:01 alan:02 data:02 data:02 structures:02 Geoffrey Alan Washburn wrote: > 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. I'm not sure I agree with this- especially the proposition that unit == truth. That would make a function of the type: unit -> 'a equivelent to the proposition "If true then for all a, a", which is obviously bogus. The assumption of the Ocaml type system is that you can not form "false" theorems within the type system (these correspond to invalid types). So either this assumption is false, or unit is the void type in the Ocaml type system. More pragmatically, I don't see any situation in which void can be used where unit couldn't be used just as well, if not better. Specially, the utility of void type is strictly limited. Given a function of type void -> whatever, you can't call it- because to call it, you need to create a value of type void, and by definition the type void has no element. You can create empty data structures of type void, but (since you can't change the type held by the data structure) you can never add elements to the data structure. The type of bottom (the function that either throws an exception or never returns) in Ocaml is unit -> 'a. Note that the return type of this function, since it's completely unconstrained, can unify with any other type. Brian