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 concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 9CAE4BC0A for ; Sun, 10 Dec 2006 22:43:16 +0100 (CET) Received: from ext.lri.fr (ext.lri.fr [129.175.15.4]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id kBALhGWh020269 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Sun, 10 Dec 2006 22:43:16 +0100 Received: from smtp.lri.fr (serveur3-5 [129.175.3.5]) by ext.lri.fr (Postfix) with ESMTP id ECC3620212A; Sun, 10 Dec 2006 22:43:15 +0100 (CET) Received: from serveur9-10.lri.fr (serveur9-10 [129.175.9.10]) by smtp.lri.fr (Postfix) with ESMTP id D5EABCED98; Sun, 10 Dec 2006 22:43:15 +0100 (CET) Received: from filliatr by serveur9-10.lri.fr with local (Exim 3.36 #1 (Debian)) id 1GtWS3-0003Ve-00; Sun, 10 Dec 2006 22:43:15 +0100 MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <17788.32627.764907.571053@serveur9-10.lri.fr> Date: Sun, 10 Dec 2006 22:43:15 +0100 To: "Haoyang Wang" Cc: caml-list Subject: Re: [Caml-list] Today's inflamatory opinion: exceptions are bad In-Reply-To: References: <004501c71c40$b52e8d00$15b2a8c0@wiko> <17788.2858.414320.138285@serveur9-10.lri.fr> X-Mailer: VM 7.19 under Emacs 21.4.1 From: Jean-Christophe Filliatre X-Virus-Scanned: by amavisd-new at lri.fr X-Miltered: at concorde with ID 457C7F74.001 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; filliatre:01 filliatr:01 lri:01 timings:01 coq:01 coq:01 typing:01 caml-list:01 kernel:01 exceptions:01 exceptions:01 caml:02 contributed:02 benchmark:02 types:03 > > # Use exceptions only for exceptional situations. May be I've been misunderstood in my quote of Kernighan & Pike. I simply think that there is no need to use exceptions when "exceptional" cases are as frequent as "normal" ones. As others already said, using option types is a good alternative. And the efficiency is similar (it happens that I recently made a benchmark on this particular point and I found out equivalent timings). > Even today, exceptions are used heavily in coq. Could you comment on > your experiences with the usage of caml exceptions in coq? Are > exceptions raised there "only for exceptional situations"? The Coq proof assistant has been developed by many people and I only contributed to a small part of it (mostly in the kernel). For this part, at least, it is indeed true that exceptions are used only for exceptional situations, mostly to signal typing errors. They are then handled globally, at the top level of the system. -- Jean-Christophe