[m-users.] Adding impurity to Mercury code: Backtracking in IO states

[Paul Bone]

On Sun, Jun 28, 2015 at 01:32:12PM +0200, Tomas By wrote:
> On Sun, June 28, 2015 07:34, Left Right wrote:
> > In particular,
> > io.write_string needs its third argument to be instantiated as
> > "unique" (this is a Mercury's way of saying it has to be obtained from
> > doing some other I/O).
> 
> I think it is just an historical accident that Mercury only uses unique
> modes for I/O.

No it's deliberate.

Uniqueness and determinism work together to make IO pure.  Without either
one of them for IO Mercury would not be a declaratively pure language.

For example, if IO states were not unique I could do:

main(IO0, IO) :-
    print("Hello ", IO0, IO1),
    print("world!", IO0, IO).

What is the result of this?  Do we have to turn back time: undo print hello
so that I can get IO0 to print world?  Or do we ignore the printing of
hello.  It becomes more awkward if the second print is replaced with
something like an if-then-else, especially an if-then-else that depends on
the result of an earlier IO action.

If we didn't have determinism for IO then programs like the following would
cause problems.

main(IO0, IO) :-
    some_nondet_code(...),
    print("Hello world!", !IO),
    soem_code_that_may_fail(...).

If the third line fails then execution backtracks to the nondet code that
may have created a choicepoint.  It needs to "undo" the IO action which
cannot be done.  or do the IO action multiple times (hopefully it's not
charging your credit card!).

Hope this helps.

-- 
Paul Bone
http://www.bone.id.au