Re: [Caml-list] Uncaught exceptions in function type.

[Romain Bardou <romain.bardou@inria.fr>]

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