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 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 62EF3BC69 for ; Mon, 30 Jul 2007 15:41:44 +0200 (CEST) Received: from wa-out-1112.google.com (wa-out-1112.google.com [209.85.146.183]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l6UDfgoZ002545 for ; Mon, 30 Jul 2007 15:41:43 +0200 Received: by wa-out-1112.google.com with SMTP id m34so2091736wag for ; Mon, 30 Jul 2007 06:41:41 -0700 (PDT) DKIM-Signature: a=rsa-sha1; c=relaxed/relaxed; d=gmail.com; s=beta; h=domainkey-signature:received:received:message-id:date:from:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; b=RQhwFIRmxIUygPMGpArlor4cX385PyvoXhwJ5SPjsSqUlZnSyqXDsIZSnKz9TNOw9ve4O+o0JOdLRriOv1ESLJmtkh1OpK5wu2QjAOSbrn/78UDw2Ej56gPN7L5MYVR48UBd5bejAE7J5qiVR3rj90s2T5AYJrkCThwI8O1q/04= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; b=EgAVtcm+qoBbPYoDG/hi9wVD+f4M+SNiAfk1ZYLsyDTBHHdvJ8kIClnVOqZfdwJLCkO35pkd25MkU3FSf8GElZn0kBtgMZME4UfOhh8l912Ep3KX+TLMiUd0bWzLasYN/Lcx+7koipxG+ncHVJKj2CKeVkjsVqWuxszYJloYoYA= Received: by 10.114.56.1 with SMTP id e1mr5579516waa.1185802901717; Mon, 30 Jul 2007 06:41:41 -0700 (PDT) Received: by 10.114.235.10 with HTTP; Mon, 30 Jul 2007 06:41:41 -0700 (PDT) Message-ID: <875c7e070707300641j300202b3q8e4d82117742d516@mail.gmail.com> Date: Mon, 30 Jul 2007 09:41:41 -0400 From: "Chris King" 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-j-chkmail-Score: MSGID : 46ADEA96.002 on discorde : j-chkmail score : X : 0/20 1 0.000 -> 1 X-Miltered: at discorde with ID 46ADEA96.002 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; ocaml:01 theorems:01 o'caml's:01 runtime:01 runtime:01 typecheck:01 wrote:01 exception:01 exception:01 caml-list:01 exceptions:01 caml:02 structures:02 construct:02 unit:03 On 7/30/07, Brian Hurt wrote: > 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). Hence why (as you point out) any function which inhabits that type must either throw an exception, abort the program, or loop, each of which are a signal that there is a logical error in the program (ignoring the use of exceptions as control structures). But since O'Caml's type system is not as powerful as, say, Coq's, it must let such propositions through and instead catch them at runtime. Take for example List.hd: 'a list -> 'a. This is not a valid proposition, since it claims we can construct any value from the empty list. But everything's OK, since Caml deals with this situation by raising an exception at runtime. The type system only lets List.hd typecheck because it's perfectly aware that, thanks to its call to "failure", it will never follow an execution path which triggers this inconsistency. - Chris