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.1 required=5.0 tests=AWL autolearn=disabled version=3.1.3 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id EFD61BC0A for ; Fri, 22 Dec 2006 21:17:49 +0100 (CET) Received: from host15.ipowerweb.com (host15.ipowerweb.com [66.235.219.115]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id kBMKHmiL016232 (version=TLSv1/SSLv3 cipher=EDH-RSA-DES-CBC3-SHA bits=168 verify=NO) for ; Fri, 22 Dec 2006 21:17:49 +0100 Received: from c-24-9-123-251.hsd1.co.comcast.net ([24.9.123.251] helo=apotheon.com) by host15.ipowerweb.com with esmtp (Exim 4.52) id 1Gxqps-0004AU-Qp for caml-list@yquem.inria.fr; Fri, 22 Dec 2006 12:17:45 -0800 Received: by apotheon.com (Postfix, from userid 1000) id 56C7D333CC; Fri, 22 Dec 2006 13:17:25 -0700 (MST) Date: Fri, 22 Dec 2006 13:17:25 -0700 From: Chad Perrin To: caml-list@yquem.inria.fr Subject: Re: strong/weak typing terminology (was Re: [Caml-list] Scripting in ocaml) Message-ID: <20061222201725.GC23003@apotheon.com> References: <458AA143.3090303@hq.idt.net> <20061221202520.GG9440@apotheon.com> <20061221221650.GL9440@apotheon.com> <3EC73FC3-41A6-4FB1-9549-29286A6568CC@epfl.ch> <1166811403.6555.46.camel@rosella.wigram> <4E1EAAC5-DC08-4A55-9AEB-0D5D3BE1C0EA@epfl.ch> <1166816522.7448.45.camel@rosella.wigram> <458C39FD.7090409@davidb.org> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <458C39FD.7090409@davidb.org> User-Agent: Mutt/1.5.13 (2006-08-11) X-Antivirus-Scanner: Clean mail though you should still use an Antivirus X-AntiAbuse: This header was added to track abuse, please include it with any abuse report X-AntiAbuse: Primary Hostname - host15.ipowerweb.com X-AntiAbuse: Original Domain - yquem.inria.fr X-AntiAbuse: Originator/Caller UID/GID - [47 12] / [47 12] X-AntiAbuse: Sender Address Domain - apotheon.com X-Source: X-Source-Args: X-Source-Dir: X-Miltered: at concorde with ID 458C3D6C.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; ocaml:01 dumped:01 restrictive:01 compiler:01 statically:01 type-safe:01 sig:01 wrote:01 wrote:01 typing:01 exception:01 caml-list:01 instances:02 subsets:02 bounds:02 On Fri, Dec 22, 2006 at 12:03:09PM -0800, David Brown wrote: > skaller wrote: > > > This is not my understanding of what safe means. > > > Your program is safe? Ok, so would you use it to > > control a nuclear reactor? Do you really think anyone > > cares if the reactor blows, whether the program > > core dumped, failed to core dump, or threw an exception? > > > > to me safe means 'cannot fail'. But perhaps i misunderstand: > > it would be interesting to see another definition. > > This is certainly a good definition of "safety", but not one commonly > used when referring to type systems. It also has problems with > undecidability, and trying to enforce it generally results in > programming languages or language subsets that are so restrictive that > general purpose programming becomes very tedius, or just impossible. > Even systems that put a lot of effort into this kind of safety (such > as SPARKAda) don't claim that they "cannot fail", but instead refer to > it as high-integrity. > > Most references use phrases like "type safety", although this seems to > get different definitions depending on the user. Although specific > instances in a program, the compiler might be able to statically > determine if an array bounds is going to be violated, this can't be > done in the general case. This all seems rather simple to me: It's type-safe if you cannot get type errors without subverting the type system. -- CCD CopyWrite Chad Perrin [ http://ccd.apotheon.org ] This sig for rent: a Signify v1.14 production from http://www.debian.org/