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.2 required=5.0 tests=AWL,SPF_NEUTRAL autolearn=disabled version=3.1.3 Received: from discorde.inria.fr (discorde.inria.fr [192.93.2.38]) by yquem.inria.fr (Postfix) with ESMTP id ADF9EBC69 for ; Mon, 30 Jul 2007 19:58:14 +0200 (CEST) Received: from nz-out-0506.google.com (nz-out-0506.google.com [64.233.162.237]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l6UHwDhC027204 for ; Mon, 30 Jul 2007 19:58:14 +0200 Received: by nz-out-0506.google.com with SMTP id z3so959711nzf for ; Mon, 30 Jul 2007 10:58:13 -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=YnDyFligwTEz0p2SLRKD6c1F2P9yyscdxCnOVt6b6tLCzUjnUZhkPgOdBPdxzw6AocASSQ7z6pwRcFcEuQfIWo2h/H/jVkGLI2rs3Nf0fZ2NUU9FDPU1uYE0YMNYFKRfdzFIkuqG51QeIm3VwkeZXbspOzuR2JiGMFoZo2703VQ= 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=QOTH578AUHMxi1iEmqkRoLAms6LnfMlQgiKis7aXnI9JLc+aFQx5DTf9q981QZmg20HA+dhcOW4pbdMlWSo0lG95gzHFpvnVzyIpBRRwY6rz3a8rOutL6Qj2tPSvHoP9OKXNJSctOHl2+r0lXPduuTI0bN1c5FFCKkO3JCiD750= Received: by 10.142.185.13 with SMTP id i13mr233364wff.1185818292405; Mon, 30 Jul 2007 10:58:12 -0700 (PDT) Received: by 10.142.255.12 with HTTP; Mon, 30 Jul 2007 10:58:12 -0700 (PDT) Message-ID: Date: Mon, 30 Jul 2007 13:58:12 -0400 From: "Markus Mottl" 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 : 46AE26B5.000 on discorde : j-chkmail score : X : 0/20 1 0.000 -> 1 X-Miltered: at discorde with ID 46AE26B5.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; markus:01 mottl:01 markus:01 mottl:01 ocaml:01 theorems:01 ocaml:01 model:01 lambda:01 derivation:01 satisfiable:01 terminating:01 model:01 trivial:01 satisfiable:01 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. Indeed, this proposition is impossibly true. > 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. I guess you mean that one cannot form proofs of propositions that don't have a model (i.e. an interpretation that makes the proposition true). There is a false dichotomy here. It rests on the assumption that a pure program that has such a type is a proof of the proposition whereas in fact it isn't. The assumption that programs are proofs only makes sense if every program is strongly normalizing, i.e. requires only a finite amount of evaluation (= "proof") steps. This is always the case with e.g. the pure, simply typed lambda calculus without fixed-point operator, which is strongly normalizing. Something that requires an infinite number of derivation steps cannot be considered a proof. If we constrained ourselves to programs that are proofs only, and if we required soundness, too, then there would be satisfiable propositions for which, indeed, you wouldn't be able to write down a program of corresponding type: some solvable problems would become unsolvable to us. OCaml is not unsound. It is also not incomplete in the sense that you cannot write down a terminating program for a proposition that has a model. But this unfortunately necessarily implies that you can write down programs that are not proofs, i.e. never terminate. Note that you can also write down the type "unit -> unit", which is a tautology and therefore trivially true in any interpretation. But you can still write down a program of this type that doesn't constitute a proof of the corresponding proposition irrespective of how trivial it may be: let rec f () = f (f ()) Provability and truth are two distinct concepts, you cannot conflate the two in the general case. This is a direct consequence of Goedel's incompleteness theorem. Some program may constitute a proof or not, and a type may correspond to a satisfiable proposition or not. We definitely don't want a system that allows us to write down something that is a proof of a false proposition (= unsound). We want to be able to write down a proof for every proposition that has a model (= completeness). But then we'll have to live with the presumably less awful fact that we will be able to write down non-proofs of non-truths (and truths alike)... > 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. You'll laugh, but I just actually made use of Chung-chieh Shan's trick to use polymorphic record fields in our code base. Here is a rough idea of where this may be useful: Assume you have a functor argument that defines several types and functions operating on these types. Now assume that I know that I will never want to use the module resulting from the functor application in a way that requires the use of some of these types and associated functions in the functor argument. How can I make sure that nobody will ever do something with the resulting module that violates these assumptions? E.g.: --------------------------------------------- module type ARG = sig type t type u val use_t : t -> unit val use_u : u -> t end module Func (Arg : ARG) = struct let propagate_t arg_t = Arg.use_t arg_t let propagate_u arg_u = Arg.use_u arg_u end type void = { void : 'a. 'a } module Arg = struct type t = int type u = void let use_u u = u.void let use_t t = print_int t end --------------------------------------------- If I had specified "u" as "unit" in the above example, I would need to e.g. raise an exception in "use_u" to indicate that my assumption was violated, or return a dummy value (integer) which may screw up something in the functor body, etc. But having specified the value as "void", I essentially get a proof at compile time that nobody will ever be able to misuse the module resulting from the functor application. Of course, I could restrict the signature of the resulting module, but this may be a non-trivial effort, e.g. if type "u" is used in sum types of the resulting module, etc., in which case I'd have to wrap the result in an intermediate module that translates function calls accordingly. The "void" solution on the other hand is just plain awesome and solves this problem safely and conveniently. Best regards, Markus -- Markus Mottl http://www.ocaml.info markus.mottl@gmail.com