Bonjour,

Quoting Haoyang Wang:
> ML was designed for theorem provers, and many of its features can be
> traced back to that specific purpose. I read somewhere that exception
> was introduced in ML for back-tracking, which occurs frequently during
> the normal course of trying out various tactics to prove a theorem.

I heavily use exceptions for backtracking in combinatorial  
optimization (actually it is a combination of exception raising and  
lazy values).
Same as for theorem provers, when a branch is proved sub-optimal it is  
abandoned.

> With automatic memory management, there is less need to clean up after
> an exception. Thus exceptions can be used quite freely in both Erlang
> and o'caml.

The exception based backtracking can be coupled with a garbage  
collector that on backtrack only moves the current pointer back (the  
abandoned memory is just overwritten by the subsequent computations).  
This is traditional in high performance combinatorial optimization  
languages/frameworks/engines.

Quoting Brian Hurt:
> I think I've come to the conclusion that exceptions are bad.
> In Ocaml, they're useless in many cases, and in most cases wrong.

I believe you have only shown that IO in the standard library has a  
poor design and that [try ... with] may be a bit too simple to handle  
all the useful cases (confer to Martin Jambon's extension). I  
completely agree for both points.

> There's one other use for exceptions I've seen (and done)- using them as
> non-local longjmps.  A classic example for this is a delete functions on a
> tree structure- you recurse all the way down to the leafs and discover that
> you're not deleting anything at all, what do you do?  I sometimes  
> (too often) throw an exception to jump out of the recursion back up  
> to the
> top level.

Apart from performance (because of the garbage collector being less  
stressed) that idioma has a few good properties like ensuring that two  
physically different versions of your tree are structurally different.  
In this specific case it only works at depth one (you can add the  
element back and end with two physically different trees that are  
structurally equal). But the technique is usefull for limiting memory  
consumption, ensuring uniqueness or implementing hash-consing and  
related.

       Diego Olivier