[m-dev.] cc_multi determinisms for IO state preds

[Ian MacLarty]

Hi,

I'd like to propose that we change the determinism of cc_multi
predicates in the standard library that take the IO state to det.
In particular I'm thinking of predicates such as try_io and write_cc.

My main motivation for this request is that more errors are possible
with cc_multi code than with det code.  For example consider the
following program:


:- module test.
:- interface.
:- import_module io.
:- pred main(io::di, io::uo) is cc_multi.

:- implementation.

main(!IO) :-
	handle_t(a, !IO),
	nl(!IO).

:- type t
	--->	a
	;	b.

:- pred handle_t(t::in, io::di, io::uo) is cc_multi.

handle_t(a, !IO) :-
	io.write_cc("a", !IO).
handle_t(a, !IO) :-
	io.write_string("aa", !IO).
handle_t(b, !IO) :-
	io.write_string("b", !IO).


Note the duplicate handling of the 'a' case in handle_t.  Such an error
could easily be made by copying and pasting code and wouldn't be detected
by the compiler.

I would justify the det determinism by arguing that under a suitable
interpretation of the IO state, you'll always get the same results for
the same input IO state.  In any case since an IO state can never
be repeated, whether you get the same results or not for the same input
is of little practical interest.

I realize that I can use promise_equivalent_solutions to get rid of the
cc_multiness, but my justification of this promise would also apply to
the standard library preds, so it shouldn't be necessary to make this
promise in user code.

Ian.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at csse.unimelb.edu.au
Administrative Queries: owner-mercury-developers at csse.unimelb.edu.au
Subscriptions:          mercury-developers-request at csse.unimelb.edu.au
--------------------------------------------------------------------------