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

Paul Bone paul at bone.id.au
Mon Jun 29 09:43:13 AEST 2015

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) :-
    print("Hello world!", !IO),

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

More information about the users mailing list