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