Exception handling

[Fergus Henderson]

Hi,

Following on from a recent discussion on the mercury-users mailing list,
I propose to incorporate the exception handling support that I have
developed in a new `extras/exceptions' directory in the `mercury-extras'
distribution.  The intent would be to eventually migrate it into the
Mercury standard library.

I have enclosed a copy of the interface for the proposed exception handling
module at the end of this mail.

One of the problems with the previous (informal) proposals in this
direction is that if you don't nail down the operational semantics
exactly, which we don't want to do, then the behaviour of exception
handling will be partially unspecified.  This proposal uses Mercury's
support for committed choice nondeterminism to model that in a
declarative fashion.  The interface I am proposing has a well-defined
(but nondeterministic) declarative semantics, and does not require
nailing down the operational semantics or making the declarative
semantics depend on the operational semantics.

The only remaining problem is the interaction of destructive update
and exception handling.  The proposal below is safe, in that it does
not allow unique modes to cross a point where exceptions can be caught,
except for the io__state.  The consequences of this are that
if users make use of exception handling, then they may find that

	(1) this prevents the compiler from performing destructive update
	    optimization and/or requires them to insert explicit calls to
	    copy/2
	
	(2) if they are building data structures and storing them in
	    the io__state, then they will need to be careful to ensure
	    that those data structures remain in a consistent state
	    if an exception is thrown.

However, in both cases, this is no worse than the situation in other
languages, such as Haskell, ML, Java, etc.  So I think we can consider
this problem solved too, even if the solution is perhaps not completely
ideal.

Given that these problems are solved, I think the time is ripe to include
this in the Mercury distribution; including it in mercury-extras first
is just a conservative step, so that we can gain some more experience
with using it before we put it in the standard library.

Comments?

P.S.

Tom, I know that you wrote a parser using the previous version
of my exception handling interface; I'd be interested to hear how
easy or difficult it is to update that to use the new interface shown below.

The interface is modified slightly from the one that I posted to
mercury-users; I have omitted the explicit determinism arguments,
since they are not necessary.

I plan to modify one more thing before I post a full diff for review:
I want to add an `incremental_try_all' which would be
to `try_all' as `unsorted_aggregate' is to `unsorted_solutions'.

%-----------------------------------------------------------------------------%
:- module exception.
:- interface.
:- import_module std_util, list, io.

%
% throw(Exception):
%	Throw the specified exception.
%
:- pred throw(T).
:- mode throw(in) is erroneous.

:- func throw(T) = _.
:- mode throw(in) = out is erroneous.

% The following types are used by try/3 and try/5.

:- type exception_result(T)
	--->	succeeded(T)
	;	failed
	;	exception(univ).

:- inst cannot_fail
	--->	succeeded(ground)
	;	exception(ground).

%
% try(Goal, Result):
%    Operational semantics:
%	Call Goal(R).
%	If Goal(R) fails, succed with Result = failed
%	If Goal(R) succeeds, succeed with Result = succeeded(R).
%	If Goal(R) throws an exception E, succeed with Result = exception(E).
%    Declarative semantics:
%       try(Goal, Result) <=>
%               ( Goal(R), Result = succeeded(R)
%               ; not Goal(_), Result = failed
%               ; Result = exception(_)
%		).
%
:- pred try(pred(T),		    exception_result(T)).
:- mode try(pred(out) is det,       out(cannot_fail)) is cc_multi.
:- mode try(pred(out) is semidet,   out)              is cc_multi.
:- mode try(pred(out) is cc_multi,  out(cannot_fail)) is cc_multi.
:- mode try(pred(out) is cc_nondet, out)              is cc_multi.

%
% try_io(Goal, Result, IO_0, IO):
%    Operational semantics:
%	Call Goal(R, IO_0, IO_1).
%	If it succeeds, succeed with Result = succeeded(R) and IO = IO_1.
%	If it throws an exception E, succeed with Result = exception(E)
%	and with the final IO state being whatever state resulted
%	from the partial computation from IO_0.
%    Declarative semantics:
%	try_io(Goal, Result, IO_0, IO) <=>
%		( Goal(R, IO_0, IO), Result = succeeded(R)
%		; Result = exception(_)
%		).
%
:- pred try_io(pred(T, io__state, io__state), exception_result(T),
						io__state, io__state).
:- mode try_io(pred(out, di, uo) is det,      out(cannot_fail),
						di, uo) is cc_multi.
:- mode try_io(pred(out, di, uo) is cc_multi, out(cannot_fail),
						di, uo) is cc_multi.

%
% try_all(Goal, ResultList):
%    Operational semantics:
%	Try to find all solutions to Goal(R), using backtracking.
%	Collect the solutions found in the ResultList, until
%	the goal either throws an exception or fails.
%	If it throws an exception, put that exception at the end of
%	the ResultList.
%    Declaratively:
%       try_all(Goal, ResultList) <=>
%		(if
%			list__reverse(ResultList, [Last | AllButLast]),
%			Last = exception(_)
%		then
%			all [M] (list__member(M, AllButLast) =>
%				(M = succeeded(R), Goal(R))),
%		else
%			all [M] (list__member(M, ResultList) =>
%				(M = succeeded(R), Goal(R))),
%			all [R] (Goal(R) =>
%				list__member(succeeded(R), ResultList)),
%		).

:- pred try_all(pred(T), list(exception_result(T))).
:- mode try_all(pred(out) is det,     out(try_all_det))     is cc_multi.
:- mode try_all(pred(out) is semidet, out(try_all_semidet)) is cc_multi.
:- mode try_all(pred(out) is multi,   out(try_all_multi))   is cc_multi.
:- mode try_all(pred(out) is nondet,  out(try_all_nondet))  is cc_multi.

:- inst [] ---> [].
:- inst try_all_det ---> [cannot_fail].
:- inst try_all_semidet ---> [] ; [cannot_fail].
:- inst try_all_multi ---> [cannot_fail | try_all_nondet].
:- inst try_all_nondet == list_skel(cannot_fail).

%
% rethrow(ExceptionResult):
%	Rethrows the specified exception result
%	(which should be of the form `exception(_)',
%	not `succeeded(_)' or `failed'.).
%
:- pred rethrow(exception_result(T)).
:- mode rethrow(in) is erroneous.

:- func rethrow(exception_result(T)) = _.
:- mode rethrow(in) = out is erroneous.

%-----------------------------------------------------------------------------%

--
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.