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=none 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 8139DBC69 for ; Mon, 30 Jul 2007 19:43:11 +0200 (CEST) Received: from smtp2-g19.free.fr (smtp2-g19.free.fr [212.27.42.28]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l6UHhBZv023419 for ; Mon, 30 Jul 2007 19:43:11 +0200 Received: from smtp2-g19.free.fr (localhost.localdomain [127.0.0.1]) by smtp2-g19.free.fr (Postfix) with ESMTP id 072A298F8B; Mon, 30 Jul 2007 19:43:11 +0200 (CEST) Received: from Tocksi.local (lns-bzn-61-82-250-75-122.adsl.proxad.net [82.250.75.122]) by smtp2-g19.free.fr (Postfix) with ESMTP id C18A998DDC; Mon, 30 Jul 2007 19:43:10 +0200 (CEST) Message-ID: <46AE2327.4090904@univ-savoie.fr> Date: Mon, 30 Jul 2007 19:43:03 +0200 From: Christophe Raffalli User-Agent: Thunderbird 2.0.0.5 (Macintosh/20070716) MIME-Version: 1.0 To: Brian Hurt , caml-list@yquem.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> <46ADE367.8020801@janestcapital.com> In-Reply-To: <46ADE367.8020801@janestcapital.com> Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 7bit X-Miltered: at discorde with ID 46AE232F.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; christophe:01 raffalli:01 christophe:01 raffalli:01 univ-savoie:01 ocaml:01 theorems:01 ocaml:01 subtyping:01 caml-list:01 surprising:01 match:02 unit:03 unit:03 pattern:04 > > > 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. > Personnally, I think that we should have more subtyping than in OCaml. Then, "void" is the smallest type (and quite equivalent to 'a.'a) and "unit" is the bigest type. This looks natural for "void" and more surprising for "unit", but you can see that you can do nothing with a value of type unit (except matching it, which is not much), which mean that is you do not match unit (you use "_" everywhere you would use "()" in pattern), then any value can be safely cast to the unit type ... So "void" is really the dual of "unit" and they are very distinct. Christophe PS: In PML it works like that (our server is down, so please wait tomorrow if you want to try PML)