[m-users.] spawn in Rosettacode

[Mark Brown]

Hi,

On Sat, Aug 30, 2014 at 4:36 PM, Robert Smart
<robert.kenneth.smart at gmail.com> wrote:
> I don't see print_cc/1.
>
> I assumed that print_cc("Rosetta\n") was a sort of partial application and
> that spawn would complete that with the !IO parameters.

Yes, that's correct. The relationship between the I/O arguments to
thread.spawn and the I/O arguments to io.print_cc is documented above
thread.spawn:

    % spawn(Closure, IO0, IO) is true iff `IO0' denotes a list of I/O
    % transactions that is an interleaving of those performed by `Closure'
    % and those contained in `IO' - the list of transactions performed by
    % the continuation of spawn/3.
    %
:- pred spawn(pred(io, io)::in(pred(di, uo) is cc_multi),
    io::di, io::uo) is cc_multi.

I/O values can be interpreted as continuations - lists of all the
primitive I/O operations that will be performed. Consider the
following slightly simplified example, for which I've expanded out the
state variables for clarity:

    p(IO0, IO) :-
        spawn(a, IO0, IO1),
        spawn(b, IO1, IO2),
        spawn(c, IO2, IO).

Let the continuation after calling be be just a call to q, and assume
a, b, c and q are primitive operations. So we have:

    IO = [q]

Then, from the meaning of spawn, IO2 is an interleaving of [c] and
[q], for which there are two possibilities:

    IO2 is in {[c, q], [q, c]}

Likewise, IO1 is an interleaving of [b] and IO2, so there are 3! possibilities:

    IO1 is in {[b, c, q], [c, b, q], [c, q, b], [b, q, c], [q, b, c], [q, c, b]}

It should be clear that IO0 is one of the 4! possible orderings of a,
b, c and q.

Also note that the order of calls to spawn would make no difference in
this semantics.

Cheers,
Mark.