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 mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id DB72CBC69 for ; Thu, 4 Oct 2007 01:22:02 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAITAA0fAXQInemdsb2JhbACONwEBCQo X-IronPort-AV: E=Sophos;i="4.21,226,1188770400"; d="scan'208";a="2099016" Received: from concorde.inria.fr ([192.93.2.39]) by mail1-smtp-roc.national.inria.fr with ESMTP; 04 Oct 2007 01:22:02 +0200 Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l93NM11T026836 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Thu, 4 Oct 2007 01:22:02 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAITAA0eCcUBTmWdsb2JhbACONwEBAQEHBAYHCBY X-IronPort-AV: E=Sophos;i="4.21,226,1188770400"; d="scan'208";a="3719959" Received: from sigma957.cis.mcmaster.ca ([130.113.64.83]) by mail3-smtp-sop.national.inria.fr with ESMTP; 04 Oct 2007 01:22:01 +0200 Received: from Dura7.UTS.McMaster.CA (dura7.UTS.mcmaster.ca [130.113.196.62]) by sigma957.cis.mcmaster.ca (8.13.7/8.13.7) with ESMTP id l93NLp3d029649; Wed, 3 Oct 2007 19:21:56 -0400 (EDT) Received: from cgpsrv2.cis.mcmaster.ca (univmail.CIS.mcmaster.ca [130.113.64.46]) by Dura7.UTS.McMaster.CA (8.13.7/8.13.7) with ESMTP id l93NLG3R001520; Wed, 3 Oct 2007 19:21:16 -0400 Received: from [99.235.248.61] (account carette@univmail.cis.mcmaster.ca HELO [192.168.1.100]) by cgpsrv2.cis.mcmaster.ca (CommuniGate Pro SMTP 4.3.12) with ESMTPSA id 187810853; Wed, 03 Oct 2007 19:21:16 -0400 Message-ID: <47042202.4070906@mcmaster.ca> Date: Wed, 03 Oct 2007 19:13:06 -0400 From: Jacques Carette Organization: McMaster University User-Agent: Thunderbird 1.5.0.8 (Windows/20061025) MIME-Version: 1.0 To: skaller Cc: caml-list@inria.fr Subject: Re: [Caml-list] Unsoundness is essential References: <20071003083529.40DA2A99F@Adric.metnet.fnmoc.navy.mil> <4703FDEF.7030900@univ-savoie.fr> <1191451810.7218.86.camel@rosella.wigram> In-Reply-To: <1191451810.7218.86.camel@rosella.wigram> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-PMX-Version-Mac: 5.3.3.310218, Antispam-Engine: 2.5.2.313940, Antispam-Data: 2007.10.3.155423 X-PerlMx-Spam: Gauge=IIIIIII, Probability=7%, Report='__CT 0, __CTE 0, __CT_TEXT_PLAIN 0, __HAS_MSGID 0, __MIME_TEXT_ONLY 0, __MIME_VERSION 0, __SANE_MSGID 0, __USER_AGENT 0' X-Miltered: at concorde with ID 47042419.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; inference:01 type-safe:01 statically:01 run-time:01 annotations:01 violate:01 run-time:01 assertion:01 ocaml:01 gcc:01 -wall:01 -pedantic:01 dumped:01 annotations:01 wrote:01 skaller wrote: > 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. > No, that's wrong. Any *complete* type system that strong is unsound. It says nothing about incomplete systems. My position is that looking for decision procedures everywhere is what is blocking real progress. People doing dependent types have gotten over most of that. > I want an unsound type system! No you don't, you want an incomplete one. You want one where the type system will tell you when you are obviously wrong, and will ask you for a proof when it's not sure. If you insist on unsound, then when the type system doesn't know, it might let things through anyways, and then all bets are off. I don't want that. > 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. > Again, I disagree. It's much better to do most type checks statically, and then to residualize some type checks to run-time if you absolutely must. This is roughly what my Master's student Gordon Uszkay did for a "scientific computation" language, using CHRs. Unfortunately, his work was already way too ambitious as it was, so all he succeeded in doing is an implementation [that works], but no formal proofs. > 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. I would rather say that what should be done is that run-time type checks should be residualized into the program, so that no unsound program would be allowed to run to completion, an assertion would be triggered first. > In fact, the idea of C is the right one. When I was forced to write a C program (after enjoying Ocaml so much), and even with gcc -W -Wall -Werror -pedantic something.c I got a clean compile which, when run, core dumped, I was seriously unhappy. > 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 > Here we agree. Both of those types are 'cheating'. Jacques