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 é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 > > > > > -- > 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 >