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 5839F7EE5B for ; Mon, 26 May 2014 16:55:10 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of romain.bardou@inria.fr) identity=pra; client-ip=87.98.165.38; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="romain.bardou@inria.fr"; x-sender="romain.bardou@inria.fr"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of romain.bardou@inria.fr) identity=mailfrom; client-ip=87.98.165.38; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="romain.bardou@inria.fr"; x-sender="romain.bardou@inria.fr"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mo2.mail-out.ovh.net) identity=helo; client-ip=87.98.165.38; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="romain.bardou@inria.fr"; x-sender="postmaster@mo2.mail-out.ovh.net"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AhIEAKBUg1NXYqUmlWdsb2JhbABZsXSRPoMNAQIBgSgOAQEBAQkLCQkSKoIlAQEFeBELGAkWDwkDAgECAUUTCAKIQgHYSBeOHzoWhCoBA5lzhxSPTQ X-IPAS-Result: AhIEAKBUg1NXYqUmlWdsb2JhbABZsXSRPoMNAQIBgSgOAQEBAQkLCQkSKoIlAQEFeBELGAkWDwkDAgECAUUTCAKIQgHYSBeOHzoWhCoBA5lzhxSPTQ X-IronPort-AV: E=Sophos;i="4.98,913,1392159600"; d="scan'208";a="76438629" Received: from 6.mo2.mail-out.ovh.net (HELO mo2.mail-out.ovh.net) ([87.98.165.38]) by mail2-smtp-roc.national.inria.fr with ESMTP; 26 May 2014 16:55:09 +0200 Received: from mail99.ha.ovh.net (b6.ovh.net [213.186.33.56]) by mo2.mail-out.ovh.net (Postfix) with SMTP id A1B4BFF982A for ; Mon, 26 May 2014 16:55:09 +0200 (CEST) Received: from b0.ovh.net (HELO queueout) (213.186.33.50) by b0.ovh.net with SMTP; 26 May 2014 16:55:09 +0200 Received: from unknown (HELO ?10.1.202.10?) (postmaster@doomeer.com@194.254.61.161) by ns0.ovh.net with SMTP; 26 May 2014 16:55:01 +0200 Message-ID: <53835610.9050609@inria.fr> Date: Mon, 26 May 2014 16:56:16 +0200 From: Romain Bardou 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: X-Enigmail-Version: 1.6+git0.20140323 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Ovh-Tracer-Id: 6180346065664576032 X-Ovh-Remote: 194.254.61.161 () X-Ovh-Local: 213.186.33.20 (ns0.ovh.net) X-OVH-SPAMSTATE: OK X-OVH-SPAMSCORE: 0 X-OVH-SPAMCAUSE: gggruggvucftvghtrhhoucdtuddrfeejvddrheekucetufdoteggodetrfcurfhrohhfihhlvgemucfqggfjnecuuegrihhlohhuthemuceftddtnecu X-Spam-Check: DONE|U 0.5046/N X-VR-SPAMSTATE: OK X-VR-SPAMSCORE: 0 X-VR-SPAMCAUSE: gggruggvucftvghtrhhoucdtuddrfeejvddrheekucetufdoteggodetrfcurfhrohhfihhlvgemucfqggfjnecuuegrihhlohhuthemuceftddtnecu X-Validation-by: romain@bardou.fr Subject: Re: [Caml-list] Uncaught exceptions in function type. On 26/05/2014 16:23, Philippe Veber wrote: > 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. > > Some issues: - One needs to separate exceptions into two groups, the ones that you are actually interested in typing (their purpose is to kill the program, so to speak) and the ones that you are not (they are actually used for control flow). - I'm not sure it is easy to infer. For instance, in: let f g = g 1 should we just assume that g raises nothing? Or should we use some kind of row variable, like: let f (g: 'a raise ([< ] as 'raises): 'b raise 'raises = g 1 But then what about: let f (g: 'a raise ([< ] as 'raises_h) (h: 'a raise ([< ] as 'raises_g): 'b raise [ 'raises_g | 'raises_h ] = g 1 + h 2 is it sound to have those abstract union types [ 'raises_g | 'raises_h ]? Do we want all functions to have these convoluted types? -- Romain Bardou