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 77F7FBC69 for ; Fri, 5 Oct 2007 00:23:59 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAADEFBUfLENaMnmdsb2JhbACOOAEBAQEHBAYp X-IronPort-AV: E=Sophos;i="4.21,232,1188770400"; d="scan'208";a="3770482" Received: from discorde.inria.fr ([192.93.2.38]) by mail3-smtp-sop.national.inria.fr with ESMTP; 05 Oct 2007 00:23:58 +0200 Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l94MNunE020015 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Fri, 5 Oct 2007 00:23:56 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAADEFBUfLENaMnmdsb2JhbACOOAEBAQEHBAYp X-IronPort-AV: E=Sophos;i="4.21,232,1188770400"; d="scan'208";a="3770481" Received: from ipmail01.adl2.internode.on.net ([203.16.214.140]) by mail3-smtp-sop.national.inria.fr with ESMTP; 05 Oct 2007 00:23:43 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAA0DBUd5LHvc/2dsb2JhbAAM X-IronPort-AV: E=Sophos;i="4.21,232,1188743400"; d="scan'208";a="204386010" 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 07:53:38 +0930 Subject: Re: [Caml-list] Unsoundness is essential From: skaller To: rossberg@ps.uni-sb.de Cc: caml-list@inria.fr In-Reply-To: <60599.84.159.34.129.1191532048.squirrel@www.ps.uni-sb.de> References: <20071003083529.40DA2A99F@Adric.metnet.fnmoc.navy.mil> <4703FDEF.7030900@univ-savoie.fr> <1191451810.7218.86.camel@rosella.wigram> <59808.84.159.34.129.1191520580.squirrel@www.ps.uni-sb.de> <1191527775.7078.67.camel@rosella.wigram> <60599.84.159.34.129.1191532048.squirrel@www.ps.uni-sb.de> Content-Type: text/plain Date: Fri, 05 Oct 2007 08:23:37 +1000 Message-Id: <1191536617.7771.18.camel@rosella.wigram> Mime-Version: 1.0 X-Mailer: Evolution 2.10.1 Content-Transfer-Encoding: 7bit X-Miltered: at discorde with ID 470567FC.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; 0200,:01 rossberg:01 statically:01 integers:01 reals:01 ocaml:01 ill-formed:01 semantics:01 integers:01 ocaml:01 semantically:01 sourceforge:01 wrote:01 wrote:01 dynamically:01 On Thu, 2007-10-04 at 23:07 +0200, rossberg@ps.uni-sb.de wrote: > skaller wrote: > > > >> Exceptions are /trapped/ errors. > > > > I chose not to accept that definition. I use instead > > "trapped at compile time", meaning "in advance of running > > the program". > > As a definition for what? What trapped means. > > Otherwise you could say dynamically typed languages were > > strongly typed and sound. > > In fact, technically, they are. People have used the term "unityped" for it. That isn't what I meant at all. Python is statically unityped, but dynamically it has integers, reals, strings, etc. Type errors in Python are not 'trapped' .. they're impossible. > > C/C++ does this right: if a program is 'ill-formed' then > > a diagnostic must be issued. Throwing an exception silently > > is NOT allowed. [C/C++ doesn't mandate diagnostics always because > > some are too hard to detect] > > This paragraph sounds like a contradiction in itself. Yes, but it isn't. If the specification was to throw a catchable exception, then that would be a requirement on implementation which would permit programmers to divide by zero deliberately. In that case, a divide by zero error is impossible to detect because it can't be distinguished from the legitimate division by zero for the purpose of raising an exception. > More importantly, an OCaml program performing div 0 isn't "ill-formed", it > has a perfectly well-defined, safe semantics (in precisely the same way as > adding a string in Python). See the library docs. I didn't claim otherwise: I claim it is a very bad idea to permit a program to do obvious bullshit like divide by zero (for integers I mean). Note I'm NOT saying Ocaml *implementation* shouldn't raise an exception, just that the language specification should not require it do so. The difference is in one case the operation is semantically well defined and thus definitely not detectable as an error, whereas in the other it is not defined, and so is unequivocably an error. Oh well this was fun but I'm off interstate without a computer for a week.. hope my Airbus doesn't divide any empty lists by zero .. -- John Skaller Felix, successor to C++: http://felix.sf.net