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 discorde.inria.fr (discorde.inria.fr [192.93.2.38]) by yquem.inria.fr (Postfix) with ESMTP id 5B98DBC69 for ; Mon, 30 Jul 2007 15:35:21 +0200 (CEST) Received: from ciao.gmane.org (main.gmane.org [80.91.229.2]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l6UDZKxs001017 (version=TLSv1/SSLv3 cipher=AES256-SHA bits=256 verify=NO) for ; Mon, 30 Jul 2007 15:35:21 +0200 Received: from list by ciao.gmane.org with local (Exim 4.43) id 1IFVP2-0007jl-CK for caml-list@inria.fr; Mon, 30 Jul 2007 15:35:16 +0200 Received: from seasnet-38-068.seas.upenn.edu ([158.130.38.77]) by main.gmane.org with esmtp (Gmexim 0.1 (Debian)) id 1AlnuQ-0007hv-00 for ; Mon, 30 Jul 2007 15:35:16 +0200 Received: from geoffw by seasnet-38-068.seas.upenn.edu with local (Gmexim 0.1 (Debian)) id 1AlnuQ-0007hv-00 for ; Mon, 30 Jul 2007 15:35:16 +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 09:35:00 -0400 Message-ID: <46ADE904.9060906@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> <46AD6CAD.7000500@cis.upenn.edu> <46ADE367.8020801@janestcapital.com> 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: seasnet-38-068.seas.upenn.edu User-Agent: Thunderbird 2.0.0.6pre (X11/20070729) In-Reply-To: <46ADE367.8020801@janestcapital.com> Sender: news X-Miltered: at discorde with ID 46ADE918.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; isomorphism:01 ocaml:01 theorems:01 ocaml's:01 recursion:01 ocaml:01 unify:01 subtyping:01 logics:01 wrote:01 upenn:01 exception:01 unsafe:01 int:01 alan:02 Brian Hurt wrote: > I'm not sure I agree with this- especially the proposition that unit == > truth. There really isn't anything to disagree with. That is how the Curry-Howard Isomorphism is defined. > 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). Firstly, as I said, OCaml's type system cannot be treated as a consistent logic: A logic where false cannot be proven. This is a consequence of its many impure language features (including general recursion). However, there is a difference between being unsafe and not being usable as a logic. > So either this assumption is false, or unit is the > void type in the Ocaml type system. Because it is possible to prove false using the OCaml type system, it is of course possible to prove anything, including a seeming proof that unit is void. Just as you can prove that an int is a function. > 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. On the whole, the nature and utility of void is technical point that is not likely to come up typical programs. It will probably become more relevant as dependently typed languages become more mainstream. > 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. I will again point out that void and bottom should not be conflated. Bottom is only really relevant in languages with subtyping, and does not have a logic interpretation in traditional logics.