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=AWL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id C482FBC69 for ; Thu, 4 Oct 2007 16:49:26 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAHeaBEfAXQImh2dsb2JhbACOOAEBCQon X-IronPort-AV: E=Sophos;i="4.21,230,1188770400"; d="scan'208";a="3753315" Received: from discorde.inria.fr ([192.93.2.38]) by mail3-smtp-sop.national.inria.fr with ESMTP; 04 Oct 2007 16:49:26 +0200 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l94EnPIF017420 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Thu, 4 Oct 2007 16:49:26 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAHeaBEfLENaMnmdsb2JhbACOOAEBAgcEBic X-IronPort-AV: E=Sophos;i="4.21,230,1188770400"; d="scan'208";a="2137253" Received: from ipmail01.adl2.internode.on.net ([203.16.214.140]) by mail1-smtp-roc.national.inria.fr with ESMTP; 04 Oct 2007 16:49:23 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAA+ZBEd5LHvc/2dsb2JhbAAM X-IronPort-AV: E=Sophos;i="4.21,230,1188743400"; d="scan'208";a="204211093" Received: from ppp121-44-123-220.lns10.syd6.internode.on.net (HELO [192.168.1.201]) ([121.44.123.220]) by ipmail01.adl2.internode.on.net with ESMTP; 05 Oct 2007 00:19:16 +0930 Subject: Re: [Caml-list] Unsoundness is essential From: skaller To: Arnaud Spiwack Cc: caml-list@inria.fr In-Reply-To: <4704AAA8.9080602@lix.polytechnique.fr> References: <20071003083529.40DA2A99F@Adric.metnet.fnmoc.navy.mil> <4703FDEF.7030900@univ-savoie.fr> <1191451810.7218.86.camel@rosella.wigram> <1191462724.7542.76.camel@rosella.wigram> <47049A6D.6020201@univ-savoie.fr> <4704AAA8.9080602@lix.polytechnique.fr> Content-Type: text/plain; charset=utf-8 Date: Fri, 05 Oct 2007 00:49:15 +1000 Message-Id: <1191509355.6518.104.camel@rosella.wigram> Mime-Version: 1.0 X-Mailer: Evolution 2.10.1 Content-Transfer-Encoding: 8bit X-Miltered: at discorde with ID 4704FD75.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; 0200,:01 ocaml:01 statically:01 non-zero:01 integers:01 compiler:01 non-zero:01 integers:01 mandates:01 notations:01 ocaml:01 non-empty:01 semantics:01 annotations:01 subtraction:01 On Thu, 2007-10-04 at 10:56 +0200, Arnaud Spiwack wrote: > Hi everybody, > Still there is something peculiar in the interpretation of Gödel > theorem, since if we are in a classical logical system (where ~~A (not > not A) and A are equivalent). If neither A nor ~A are provable, then > both can be "the real one". By that I mean that both can be chosen as > true, without impacting the consistency of the system (quick proof > sketch : A -> ~A is equivalent to A -> (A -> False) which is equivalent > to A&A -> False wich is equivalent to ~A). > > A conclusion I can draw from that is that we don't care about what is > true, we care about what is provable, since it is at least welle > defined, This is my point. Theorists have this all wrong. I'm a programmer. I do NOT really care if my program is provably correct. Sure, it would be nice to have such a proof, but the lack of one will not stop me writing the program! What I care about is that the program works. Now, suppose I code some types in my program, and the type system cannot prove I have respected them. Incompleteness ensures this can happen (given a sufficiently powerful type system). Pragmatics indicates this is also possible: the proof may indeed be constructible but take too long to construct to be practical. Should it accept or reject the program? My claim is that it should accept the program. It should only reject programs which can be proven incorrect. Now, I want you to hold on before disputing that claim, because there is more to the reasoning to come. The purpose of typing is to assist in showing a program is incorrect. We know for sure that in principle and practice there will be well typed incorrect programs, so there is no issue of proving all programs correct. The question is, should we strengthen the type systems we use to be more descriptive? There is a problem doing this. If we make the type system descriptive enough, there is a possibility we will be able to reject more programs -- this is good! But it is also likely that we will lose the ability to prove the typing is correct. What should we do? If we reject the program, the programmer will be annoyed, if we accept it, the type system is unsound, because in accepting it, we risk accepting programs which are not well typed, and therefore not correct. Now, please observe that with a stronger type system, we are going to reject more programs. That is the point. But we are ALSO going to be unable to decide the well typedness of many programs, for either incompleteness or pragmatic reasons. It simply isn't feasible to reject these programs simply because a proof of well-typedness cannot be constructed: and there is no possibility of disputing this claim because it is what programming languages like Ocaml do right now: they generate run time checks precisely because they cannot ensure correctness. It's already a known fact that today, we cannot ensure certain things like array bounds and zero division statically. So the question is, whether array length and non-zero integers should be expressible in the type systems today. And my answer is YES PLEASE. A type system with that expression MUST BE UNSOUND. I hope this argument is not too hard to follow: if you make the type system expressive enough, right now, then it MUST BE UNSOUND because we cannot have the type system rejecting the many correct programs I can and do write where I (think I) know I'm never going to divide by zero, simply because the type system cannot prove my belief. There is no issue that the powerful type system must be unsound. That is not the question or the claim. The question is: should compiler writers introduce powerful enough type systems that can express things like non-zero integers or array index correctness, KNOWING FOR SURE THAT TO DO SO MANDATES UNSOUNDNESS. There's no question such powerful type systems have to be unsound, at least today. That isn't in dispute! The question is whether we should introduce such rich and expressible notations anyhow! My claim is YES WE SHOULD. Because Arnaud is quite wrong in his belief that 'what we should care about is provability'. That is what theoreticians care about, but it is NOT the domain in which programmers operate (unless they're type systems programmers of course! :) [PS: of course I do *care* about provability, but I'm not willing to give up programming just because I can't prove everything I code is correct] So finally I will give an example: I cannot write this: hd : 'a non-empty-list -> 'a divide: int * non-zero-int -> int in Ocaml at the moment. Should I be able to?? If you say YES, you will note the Ocaml type system would become unsound. Ocaml simply cannot prove in all cases that an integer value is non-zero, nor that a list is non-empty. We do not reject programs that apply 'hd' just because of this. Heck: hd and divide ARE PART OF THE CORE LIBRARY!!!! My point is: NOTHING IS LOST BY MAKING THE TYPE SYSTEM UNSOUND WITH THIS EXTENSION. Indeed in SOME cases Ocaml may indeed be able to prove wrong typing, so we GAIN something from the point of view of machine verification. And the human programmer gains something too, because they too may find errors, even ones the type system cannot, and it could easily make the program semantics easier to understand, if the interface type annotations were richer. So my belief is that theoreticians are doing the programming industry a DISSERVICE by insisting on sound typing, because in so doing they're greatly limiting the expressiveness of the type system. There is no benefit in it. That is the point. A proof of well-typedness is NOT a proof of correctness in the first place. I do not care that the type system cannot prove well typedness because that is not its job: its job is to prove a program INCORRECT by proving wrong typing. Making the type system unsound by extending the expressiveness can be done without failing to reject programs which are currently rejected. Take Ocaml and add non-zero integers, and allow it to accept programs where the non-zeroness cannot be proven, and we are no worse off than now, where the same fact applies: Ocaml ALREADY allows such programs. Much as we'd like to be able to guarantee that a program using non-zero integer type is well typed, it is better to let such a program pass, than to compromise the expressiveness of the type system JUST BECAUSE THEORETICIANS ARE SO CONFUSED ABOUT WHAT THE PURPOSE OF THE TYPE SYSTEM IS THAT THEY REFUSE TO ALLOW AN UNSOUND ONE (of course I'm definitely not meaning to be offensive here!) If you think a type system has to be sound, you do not understand that the purpose is to catch errors early, and if not diagnose them late, and we wish to catch as many as possible. We are therefore COMPELLED to introduce a richer type system, and there is no doubt such a system, at least today if not always, cannot be sound. BTW: I am not asking for 'non-zero-int' and 'non-empty-list' as actual features for Ocaml. There is still a real issue how to make the extensions to the type system in a general enough way. For example: int \ {0} looks better because subtraction is a fairly general operator, but there may be other more useful annotations. There certainly exist languages where the 'checking' system is 'unsound'. For example Eiffel and Felix both allow pre and post conditions on functions, and both generate run time checks, which are witness to unsoundness. It is merely pride of theoreticians that they claim a precondition is not type information. There is NO DOUBT in my mind a precondition is precisely a restriction on the set of input values to a function, and is definitely type information. Ocaml does not let you notate this**, although you can write an assert, but in Felix it is plain it is intended as type information: fun divide(x: int where x!=0): ... even though this is not encoded in the type signature because I do not know what to do with it. In Felix the typing is unsound, because it generates the non-zero test at run time. ** of course Ocaml DOES let you notate this now we have private types we can enforce the constraint in the constructor of a record, however this semi-abstract type is nominally typed, and not quite the same as a structural annotation like int \ {0} which is anonymously typed. However this enforcement is clearly an unsoundness of typing because the constraint isn't enforced at compile time. So this is a perfect example of a GOOD extension of the kind I desire which already introduces an unsoundness. The key point of the idea is in fact to clearly and pointedly restrict the unsoundness to the constructor. Using this, plus smartness of the type system, we may be able to: a) reject some programs which are clearly incorrect b) optimise away the check in other programs which are clearly correct c) accept a program where the type system cannot decide and generate runtime check as witness to the unsoundness This is GOOD. There should be more of it! The lack of soundness is not a problem -- it's ESSENTIAL to rejecting even more incorrect programs because there's no way to eliminate the unsoundness without eliminating the very expressiveness which allows more programs to be type checked and thus more to be rejected. What's more, it leads to better performance too. -- John Skaller Felix, successor to C++: http://felix.sf.net