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=1.0 required=5.0 tests=AWL,SPF_NEUTRAL autolearn=disabled version=3.1.3 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 22664BC69 for ; Mon, 30 Jul 2007 15:32:25 +0200 (CEST) Received: from ik-out-1112.google.com (ik-out-1112.google.com [66.249.90.181]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l6UDWOeF007157 for ; Mon, 30 Jul 2007 15:32:24 +0200 Received: by ik-out-1112.google.com with SMTP id b35so1097254ika for ; Mon, 30 Jul 2007 06:32:24 -0700 (PDT) DKIM-Signature: a=rsa-sha1; c=relaxed/relaxed; d=gmail.com; s=beta; h=domainkey-signature:received:received:message-id:date:from:sender:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references:x-google-sender-auth; b=q/r/6hjhCCnxEIKbtkOsFiDfeu94XaEsel8jQcb4VufenylsjITT0WETCxjQS+gH0BCZ9R96PuhjwSI7QnpPAaUdQ2BKmY5ieJJ6qX6u6BriXnQDzv6yBIga+pg5wIoaDiHP9XVMKpzz7i19MNvyi4oee+Y23NHLW62Nhq9rWeI= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:sender:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references:x-google-sender-auth; b=Ps2Np/8MLZZGU8YjRF244Z4yENH1xbHDtBj7S/QrvE4xOVizbxITME8KIg/Jshe1JfnOs5ebWeq8cGPU48sdNGBu0OVETggYDfe2TVEFNNvT9HACDViLpaW5oZyhOiiAmS4lzsR88fZbcEDKSs/cg8HJTPcpKHtJ12N+TSaHoWw= Received: by 10.78.204.7 with SMTP id b7mr1494489hug.1185802344144; Mon, 30 Jul 2007 06:32:24 -0700 (PDT) Received: by 10.78.158.5 with HTTP; Mon, 30 Jul 2007 06:32:24 -0700 (PDT) Message-ID: <4a051d930707300632h1e7d9cbbta3f833f512a810db@mail.gmail.com> Date: Mon, 30 Jul 2007 09:32:24 -0400 From: "Christopher L Conway" Sender: christopherleeconway@gmail.com To: "Brian Hurt" Subject: Re: [Caml-list] Re: Void type? Cc: "Geoffrey Alan Washburn" , caml-list@inria.fr In-Reply-To: <46ADE367.8020801@janestcapital.com> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Content-Disposition: inline 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> <46ADE367.8020801@janestcapital.com> X-Google-Sender-Auth: 1cf2c85af7f08b21 X-Miltered: at concorde with ID 46ADE868.002 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; isomorphism:01 ocaml:01 ocaml:01 val:01 theorems:01 unify:01 beginner's:01 bug:01 beginners:01 wrote:01 wrote:01 arnaud:01 abstract:01 exception:01 caml-list:01 I'm no expert on this subject, but I'd like to pause this thread to point out that we have, on the one hand, people trying to explain the Curry-Howard isomorphism and, on the other, people trying to explain the pragmatics of the OCaml type system, and that it does not appear that this thread is converging towards either party comprehending the other... So... from the Curry-Howard perspective the "void" (uninhabited) type represents false, because it is a proposition (=type) that has no proofs (=values). I think (and here I'm treading on thin ice) that a type (X -> void) would represent a reductio ad absurdum proof of (not X) whereas a type (void -> X) would simply have no meaning. If you're interested in the connection between ML and Curry-Howard, and you have some spare time, you might read: research.microsoft.com/~simonpj/papers/not-not-ml/index.htm Chris On 7/30/07, Brian Hurt wrote: > 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 > > _______________________________________________ > Caml-list mailing list. Subscription management: > http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list > Archives: http://caml.inria.fr > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > >