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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 334877EE5B for ; Mon, 26 May 2014 18:05:13 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of philippe.veber@gmail.com) identity=pra; client-ip=209.85.212.181; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="philippe.veber@gmail.com"; x-sender="philippe.veber@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of philippe.veber@gmail.com designates 209.85.212.181 as permitted sender) identity=mailfrom; client-ip=209.85.212.181; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="philippe.veber@gmail.com"; x-sender="philippe.veber@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-wi0-f181.google.com) identity=helo; client-ip=209.85.212.181; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="philippe.veber@gmail.com"; x-sender="postmaster@mail-wi0-f181.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AsABAMhlg1PRVdS1lGdsb2JhbABZFoNDWKw8jFmIfAGBDAgWDgEBAQEHCwsJEiqCJQEBAQMBEgYoARsSCwEDAQsGBQQHGiEiAREBBQEKEgYTEhCICwEDCQgNozJqjRmDDZluChknAwpkhTYRAQUMjkIEB4RABIReBZEPhAGBPY95GCmCcoF4Oy8 X-IPAS-Result: AsABAMhlg1PRVdS1lGdsb2JhbABZFoNDWKw8jFmIfAGBDAgWDgEBAQEHCwsJEiqCJQEBAQMBEgYoARsSCwEDAQsGBQQHGiEiAREBBQEKEgYTEhCICwEDCQgNozJqjRmDDZluChknAwpkhTYRAQUMjkIEB4RABIReBZEPhAGBPY95GCmCcoF4Oy8 X-IronPort-AV: E=Sophos;i="4.98,913,1392159600"; d="scan'208";a="64199780" Received: from mail-wi0-f181.google.com ([209.85.212.181]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 26 May 2014 18:05:12 +0200 Received: by mail-wi0-f181.google.com with SMTP id n15so226071wiw.14 for ; Mon, 26 May 2014 09:05:11 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=s+gJBQqXj205tS48AbmUO+iRNmw/a4z59kgY7JOkquA=; b=W3w4G4UxZUSlBngI59bYdVWIWnqMVbAD0uOba4dlJpD79ESK4w3/w8I/ETP32Xz3QB 8F/c8F7hgxVQHQQOPBU4fbqGxyYMyarrbJUStDujTepAqCspHLPAqMhJPoluuvBvxDOU Y1tdJ7Jj5xQaNaJs6MstB4Vv/3DNfp5tz4tZ+PostrpWIvURAP3wuPJ6UAc1W/p9tJYm lNw6Y5P0Zy9/QOWvyk9cGIlotfYnHoUaWjulZqHiQFibIbNonkG4dvjfrLf7F44uncbL k2LOKtrtC2g8GEFrVe0TIyJ1WFpWwqHWiNqcbTtov+mRG04G5jrsatIKFa4FcXScNaNz yZSg== X-Received: by 10.194.77.72 with SMTP id q8mr28898173wjw.82.1401120311911; Mon, 26 May 2014 09:05:11 -0700 (PDT) MIME-Version: 1.0 Received: by 10.194.239.100 with HTTP; Mon, 26 May 2014 09:04:51 -0700 (PDT) In-Reply-To: <53835EB3.5050503@crans.org> References: <53835EB3.5050503@crans.org> From: Philippe Veber Date: Mon, 26 May 2014 18:04:51 +0200 Message-ID: To: Thomas Blanc Cc: caml users Content-Type: multipart/alternative; boundary=047d7bfcebd47aafce04fa4fbe78 X-Validation-by: philippe.veber@gmail.com Subject: Re: [Caml-list] Uncaught exceptions in function type. --047d7bfcebd47aafce04fa4fbe78 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Thanks a lot Thomas, this is certainly enough to satisfy my curiosity! 2014-05-26 17:33 GMT+02:00 Thomas Blanc : > Le 26/05/2014 16:23, Philippe Veber a =E9crit : > > 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 t= his >> 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=E7ois 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 > > > > > -- > Caml-list mailing list. Subscription management and archives: > https://sympa.inria.fr/sympa/arc/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > --047d7bfcebd47aafce04fa4fbe78 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
Thanks a lot Thomas, this is certainly enough to satisfy m= y curiosity!


2014-05-26 17:33 GMT+02:00 Thomas Blanc <thomas.blanc@crans.= org>:
Le 26/05/2014 16:23, Philippe Veber a =E9cri= t :

Hi everyone,

Out of curiosity, I was wondering how difficult it would be in theory to ex= tend 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 typ= e information be infered automatically? Could this be used to have an exhau= stivity 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,
=A0 Philippe.



This as already been analyzed by Fran=E7ois 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-or= der functions:
you would have to reannotate all of your .mli to add the exception annotati= ons.
([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 excepti= ons in your program, with nifty stuff like first class modules and generati= ve functors it is no longer the case.

[1] http://pauillac.inria.fr/~xleroy/publi/exception= s-popl.ps.gz




--
Caml-list mailing list. =A0Subscription management and archives:
ht= tps://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners<= /a>
Bug reports: http://caml.inria.fr/bin/caml-bugs

--047d7bfcebd47aafce04fa4fbe78--