From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 2579ABC8C for ; Thu, 27 Jan 2005 10:37:10 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j0R9b8qZ002378 for ; Thu, 27 Jan 2005 10:37:09 +0100 Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id KAA16206 for ; Thu, 27 Jan 2005 10:37:08 +0100 (MET) Received: from smtp1.adl2.internode.on.net (smtp1.adl2.internode.on.net [203.16.214.181]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j0R9b6Yo002370 for ; Thu, 27 Jan 2005 10:37:07 +0100 Received: from [192.168.1.200] (ppp205-248.lns1.syd3.internode.on.net [203.122.205.248]) by smtp1.adl2.internode.on.net (8.12.9/8.12.9) with ESMTP id j0R9YZTX006159; Thu, 27 Jan 2005 20:04:36 +1030 (CST) Subject: Re: [Caml-list] '_a From: skaller Reply-To: skaller@users.sourceforge.net To: Jacques Garrigue Cc: hamburg@fas.harvard.edu, caml-list In-Reply-To: <20050127.095119.88330421.garrigue@math.nagoya-u.ac.jp> References: <1448756C-6FF9-11D9-8411-0003939A19AA@fas.harvard.edu> <20050127.095119.88330421.garrigue@math.nagoya-u.ac.jp> Content-Type: text/plain Message-Id: <1106818474.6734.152.camel@pelican.wigram> Mime-Version: 1.0 X-Mailer: Ximian Evolution 1.2.2 (1.2.2-4) Date: 27 Jan 2005 20:34:35 +1100 Content-Transfer-Encoding: 7bit X-Miltered: at nez-perce with ID 41F8B645.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 41F8B642.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 sourceforge:01 wrote:01 runtime:01 expressivity:01 ocaml:01 ocaml:01 incorrectly:01 runtime:01 'real':01 enforces:01 pointer:01 debugger:01 uncaught:01 lulled:01 X-Spam-Checker-Version: SpamAssassin 3.0.0 (2004-09-13) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.0 X-Spam-Level: On Thu, 2005-01-27 at 11:51, Jacques Garrigue wrote: > There is no deep magic, no heuristics. There is just a type system > which guarantees type soundness (i.e. "well typed programs cannot > produce runtime type errors"). Unfortunately, 'soundness' as described is somewhat weaker than one would like, since it depends on the expressivity of the type system how useful soundness actually is. Ocaml can still produce run time errors for situations that 'should' have been considered type errors, except the typing is not strong enough to allow it. In the extreme, a fully dynamic type system in which everything has type 'object' has a fully sound static type system behind it, and there cannot be any run time 'type' errors in the sense of the static type. For less extreme circumstances, C++ programmers would express surprise the typing is so weak that array length is not part of an array type, so that a bounds violation is technically not a type error in Ocaml whereas in a language where the length was part of type information the very same error would indicate unsound typing. There are in fact quite a few incorrectly typed functions as well, for example List.hd and List.tl can fail at run time, but this isn't considered a type error simply because the function typing is actually wrong. Thus, 'soundness' being ensured must be taken with a grain of salt. The fact that 'well typed programs can't produce runtime *type* errors' doesn't really tell you as much as you'd like -- other errors can still occur which aren't technically type errors, but in a less 'technical' interpretation certainly are. Exceptions are part of the evil here, since they permit blatant uncontrolled lying about type. The 'real' type of List.hd is hd: 'a list -> 'a option considering it as a total function. The type hd: 'a stream -> 'a is correct but only applies to streams, which lists are not. An exception free implementation of List.hd would always produce the correct typing: let hd x = function | [] -> None | h :: _ -> Some h In effect, Ocaml first pretends unsound typing is actually sound, and then enforces this at run time by throwing an exception where one would otherwise accuse the type system of unsoundness, but claims the error is not a type error. It isn't clear whether this trick is enough to say the type system is genuinely sound. One could argue dereferencing a null pointer in C is, or is not, a type error -- either way it is a nasty error which can't be easily tracked down except by 'binary chop' on your code with diagnostics, or a debugger -- and Ocaml is no different in character when you find your code terminated with an uncaught Not_found exception. [A really nasty one is that polymorphic compare is not polymorphic .. it can't handle abstract types eg BigInt or functions .. but you'll only find out at run time ..] In practice, Ocaml really does help detect errors early that weaker languages like C++ would not, so this isn't a criticism so much as a warning: it is still possible to have a significant number of 'technical' errors in an Ocaml program (quite apart from just getting your encoding of some algorithm entirely wrong) -- and it is easy to be lulled into a false sense of security by the very fact the basic typing is both expressive and sound. -- John Skaller, mailto:skaller@users.sf.net voice: 061-2-9660-0850, snail: PO BOX 401 Glebe NSW 2037 Australia Checkout the Felix programming language http://felix.sf.net