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

[Goswin von Brederlow <goswin-v-b@web.de>]

On Mon, May 26, 2014 at 05:25:21PM +0200, Philippe Veber wrote:
> Hi Romain!
> 
> 
> > 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 would not like such a separation, unless the user can decide the kind of
> each exception (did you say burdensome? ;o). This kind of separation is
> pretty much the reason why there are errors and exceptions in Java, IIRC.

An exception that is used for control flow will be thrown and quickly
caught. It would not appear in a functions signature if the control
flow is done right. But if you made a mistake and didn't catch it then
it should appear in the signature and give you cause to recheck your
code.

I would say that exceptions used for control flow are exactly the
ones that you want typed.

On the other hand exceptions that kill the programm, like out of
memory, would be completly useless to type. Basically anything can
throw out of memory and nobody can catch it. It would simply appear in
every single (non trivial) function and annoy the programmer.

> > - 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?
> 
> No, we should assume g raises something, and that f raises the same.
> 
> 
> > Or should we use some kind
> > of row variable, like:
> >
> > let f (g: 'a raise ([< ] as 'raises): 'b raise 'raises =
> >   g 1
> >
> 
> Yes more like that
> 
> 
> >
> > 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 ]?
> >
> 
> I guess it is not easy because 'raises_g and 'raises_h may have
> incompatibilities (same constructors with different arguments). Since you
> worked on union of abstract polymorphic variant types, I guess you know
> pretty well how difficult that would be ;o).

# exception Foo of int;;
exception Foo of int
# let f () = raise (Foo 1);;
val f : unit -> 'a = <fun>
# exception Foo of float;;
exception Foo of float
# let g () = raise (Foo 1.0);;
val g : unit -> 'a = <fun>
# let h () = f () + g ();;
# let h () = let t = f () in g ();;
Warning 26: unused variable t.
val h : unit -> 'a = <fun>
# f ();;
Exception: Foo 1.
# g ();;
Exception: Foo 1..
# h ();;
Exception: Foo 1.
# try h (); 1.0 with Foo x -> x;;
Warning 21: this statement never returns (or has an unsound type.)
Exception: Foo 1.

Nothing wrong with h () raising [ Foo of int | float ] other than that
it makes it impossible to catch because Foo of int is shadowed by Foo
of float. The user couldn't catch both, the compiler would infer that
anything using h throws at least Foo of int and the user would quickly
realize that it wasn't a good idea to have to constructors with
different types. Problem solved.

Actualy infering exceptions would be a great help there. The user
might think that he caught Foo of int in the above code. The compiler
would proof him wrong highlighting the problem.



But consider the following:

let h f = let t = f () in function g -> g ()

val h : (unit -> 'a raise ([< ] as 'rf))
        -> (((unit -> 'a raise ([< ] as 'rg)) -> unit raise 'rg)) raise 'rf

Here h raises both 'rf and 'rg, just like in the above example. BUT
'rf is raised on and only on the partial application of f. This is
important when you have:

let h' f g =
  let t = try Some (f ()) with Foo x -> None in
  match t with
  | None -> None
  | Some x -> g x

The compiler has to see that (at least some of) the execptions of f
are cought and only the exceptions of g can be raised (and what isn't
cought of f).

Types can get rather comvoluted.

But hey, if they type gets to complex then maybe you should try using
less exceptions and more variant types and options. :)

> > Do we want all functions to have these convoluted types?
> >
> Representing those types could be optional most of the time. The only place
> where they would be important would when catching exceptions, to have the
> compiler check for exhaustivity.

And .mli files and signatures.

But I agree that the point of infering exceptions would be to have the
compiler check that there are none (or only the short list of allowed
exceptions).

That just leaves higher level functions. They would all have to be
convoluted.

Also would

# let f g x = g x
val f : ('a -> 'b) -> 'a -> 'b = <fun>

mean that g must not throw any exceptions? Or can the type system
infer that f will throw the same exceptions as g because no complex
exception type was specified? Can we make the "raise ([< ] as
'raises_g)" part implied? That would greatly help the transition and
cut down on convoluted types. The case of higher level functions just
passing through any exceptions would be the most common case and
should have a simple type.

MfG
	Goswin