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 A9500BC6F for ; Thu, 4 Oct 2007 00:50:24 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAHe5A0fAXQInemdsb2JhbACONwEBCQo X-IronPort-AV: E=Sophos;i="4.21,226,1188770400"; d="scan'208";a="3719199" Received: from concorde.inria.fr ([192.93.2.39]) by mail3-smtp-sop.national.inria.fr with ESMTP; 04 Oct 2007 00:50:24 +0200 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l93MoMXP024727 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Thu, 4 Oct 2007 00:50:24 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAO+5A0fLENaMn2dsb2JhbACONwEBAQEHBAYHCBg X-IronPort-AV: E=Sophos;i="4.21,226,1188770400"; d="scan'208";a="17259101" Received: from ipmail01.adl2.internode.on.net ([203.16.214.140]) by mail4-smtp-sop.national.inria.fr with ESMTP; 04 Oct 2007 00:50:22 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAANK3A0d5LHvc/2dsb2JhbAAM X-IronPort-AV: E=Sophos;i="4.21,226,1188743400"; d="scan'208";a="203654372" 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; 04 Oct 2007 08:20:11 +0930 Subject: Unsoundness is essential From: skaller To: Christophe Raffalli Cc: kirillkh , oleg@pobox.com, caml-list@inria.fr In-Reply-To: <4703FDEF.7030900@univ-savoie.fr> References: <20071003083529.40DA2A99F@Adric.metnet.fnmoc.navy.mil> <4703FDEF.7030900@univ-savoie.fr> Content-Type: text/plain Date: Thu, 04 Oct 2007 08:50:10 +1000 Message-Id: <1191451810.7218.86.camel@rosella.wigram> Mime-Version: 1.0 X-Mailer: Evolution 2.10.1 Content-Transfer-Encoding: 7bit X-Miltered: at concorde with ID 47041CAE.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; 0200,:01 christophe:01 raffalli:01 integers:01 inference:01 type-safe:01 annotations:01 violate:01 compiler:01 ocaml:01 incorrectly:01 compiler:01 casts:01 bug:01 annotations:01 On Wed, 2007-10-03 at 22:39 +0200, Christophe Raffalli wrote: > So the story is by saying (wrongly) that it is too heavy to anottate > arrow types with exceptions, > making the arrow type a ternary type construct, ML is missing a lot ... To be bold I propose type theorists have got it totally wrong. Goedel's theorem says that any type system strong enough to describe integer programming is necessarily unsound. All advanced programming languages have unsound type systems of necessity. Some falsely claim soundness by denying the expression of certain type information (eg array bounds or the type of integers excluding zero). I want an unsound type system! It much better than the useless but 'sound' type system of Python, in which the type inference engine decides all values have type Object and proves in vacuuo that all programs are type-safe, only to do the dependent type checks at run time anyhow -- a cheat known as dynamic typing. It is better to admit from the start that type systems can and MUST be unsound, and allow programmers to write known correct programs with expressive typing which no type system could type check, than to turn programmers off by rejecting their valid code. The cost is some invalid code will be accepted, but there is no help for it: the type system has to be unsound or it is of no practical use at all (Ok, I exaggerate, predicate calculus is complete and useful .. algebraic typing is the equivalent). In particular, the ability to write proper type annotations such as divide: int * (int - {0}) -> int and fail to reject programs which violate the typing is an essential and useful feature. Later, some programs may be properly rejected early instead of late when some smart type theorist extends the capabilities of the compiler, or the programmer learns how to re-express the typing so the existing algorithms catch more faults. Languages like Ocaml make significant advances in type checking capability, but users and theorists incorrectly laugh at the weak and unsound type system of C. In fact, the idea of C is the right one. We know the type system is unsound. It is essential. It is the very reason C lives on. Newer compilers have better error detection, in the meantime C doesn't stop you writing your code. C does this right: you can use a cast to override the type checks OR you can simply exploit the unsoundness directly. The latter is preferable because later versions of the compiler may be smart enough to catch real errors which the casts would always defeat. It's time to turn type theory on its head. Forget about whether the typing is sound, give me EXPRESSION first and worry about checking second. Accept Goedel: the unsoundness is *essential* and thus must not be an excuse for failure to express. Let me write: divide: int * (int - {0}) -> int and I may catch a bug using the human brain, or later the compiler may be improved and catch more bugs automatically. The fact it will never catch all these bugs is irrelevant because unsoundness is an essential requirement of expressive type systems. Stop CHEATING by refusing to allow me to write types you can't check -- because this forces ME as the programmer to cheat on the type annotations: divide: int * int -> int hd : 'a list -> 'a -- John Skaller Felix, successor to C++: http://felix.sf.net