From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 42CF87EE5B for ; Mon, 26 May 2014 17:33:54 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of thomas.blanc@crans.org) identity=pra; client-ip=138.231.136.39; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="thomas.blanc@crans.org"; x-sender="thomas.blanc@crans.org"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of thomas.blanc@crans.org) identity=mailfrom; client-ip=138.231.136.39; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="thomas.blanc@crans.org"; x-sender="thomas.blanc@crans.org"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@redisdead.crans.org) identity=helo; client-ip=138.231.136.39; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="thomas.blanc@crans.org"; x-sender="postmaster@redisdead.crans.org"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AksBAPldg1OK54gnl2dsb2JhbABZFoNDrhuUTgGBExYOAQEBAQEIFgc8giYBBRgaAQVAEQshFg8JAwIBAgFFEwgCiD4N1TAXjlkWhCoBA5VyhAGBPYUuj3Zq X-IPAS-Result: AksBAPldg1OK54gnl2dsb2JhbABZFoNDrhuUTgGBExYOAQEBAQEIFgc8giYBBRgaAQVAEQshFg8JAwIBAgFFEwgCiD4N1TAXjlkWhCoBA5VyhAGBPYUuj3Zq X-IronPort-AV: E=Sophos;i="4.98,913,1392159600"; d="scan'208";a="76449867" Received: from redisdead.crans.org ([138.231.136.39]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 26 May 2014 17:33:53 +0200 Received: from [192.168.1.107] (perens.inria.fr [128.93.60.79]) (using TLSv1 with cipher ECDHE-RSA-AES128-SHA (128/128 bits)) (No client certificate requested) by redisdead.crans.org (Postfix) with ESMTPSA id 67C9CF40 for ; Mon, 26 May 2014 17:33:52 +0200 (CEST) Message-ID: <53835EB3.5050503@crans.org> Date: Mon, 26 May 2014 17:33:07 +0200 From: Thomas Blanc User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Icedove/24.5.0 MIME-Version: 1.0 To: caml-list@inria.fr References: In-Reply-To: Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 8bit Subject: Re: [Caml-list] Uncaught exceptions in function type. Le 26/05/2014 16:23, Philippe Veber a écrit : > Hi everyone, > > Out of curiosity, I was wondering how difficult it would be in theory > to extend the type system so that exceptions that can pop out of a > function when it is called would be included in the type of the > function. Could this type information be infered automatically? Could > this be used to have an exhaustivity check in the "with" part of a try > ... with expression? > > I guess that if it was so easy, we would already be enjoying it within > our favorite compiler, but I fail to see how hairy is the question. > > Cheers, > Philippe. > > This as already been analyzed by François Pessaux and Xavier Leroy, see [1] that does a very good survey on the matter. The main problem for it is (as Romain pointed out) the problem of higher-order functions: you would have to reannotate all of your .mli to add the exception annotations. ([1] solved it by doing a separate type analysis) This would lead to a lot of problems (along with breaking existing code): * "exceptions we know won't be throwed": Typing analysis can't know that "x/2" or a.((Array.length a) - 1) wouldn't raise anything, so you'd have a lot of unexpected exceptions that would come up. * An arbitrary big number of exceptions At the time [1] was wrote, there was necessarily a finite number of exceptions in your program, with nifty stuff like first class modules and generative functors it is no longer the case. [1] http://pauillac.inria.fr/~xleroy/publi/exceptions-popl.ps.gz