[m-users.] Just saying thank you, determinism rocks.

[Zoltan Somogyi]

2021-07-28 20:05 GMT+10:00 "Volker Wysk" <post at volker-wysk.de>:
>> I still have a few grey areas about cc_multi and cc_nondet 
> 
> So do I...

The basic idea is quite simple. Nondet and multi say that a predicate
may have more than one solution, with nondet but not multi allowing
zero solutions as well. A predicate mode which is nondet or multi
will return all its solutions. If the mode is cc_nondet, that means
"this mode of this predicate may have any number of solutions,
but the implementation will stop after generating the first one,
and in terms of the declarative semantics, it is unpredicatable
which solution will be the first". Cc_multi is the same, except
for disallowing zero solutions. Operationally, you *can*predict
which solution will be the first, since Mercury does depth first search
with a left-to-right execution, though not on the raw form of
each clause body, but in its form after mode analysis reorders
the clause body to put the producer of each variable before
its consumer(s).

How you can fit cc_multi code into det code, and cc_nondet code
into semidet code, is only slightly more complicated. There are
three ways:

1. You can declare main/2 to be cc_multi, in which case all the
    code it calls outside of a negated context may be cc_multi.

2. You can quantify away all the output variables of a cc_multi
    or cc_nondet computation. The different solutions of such
    computations differ only in the values of its output variables,
    so if you ignore all of them, the solutions are indistinguishable
    from the point of the caller. A cc_multi computation whose
    outputs are quantified away is det, while a cc_nondet computation
    with outputs quantified away is semidet.

3. The third way is the tricky one. If a computation can generate
    several solutions, but they are all equally good for your purposes,
    then you can tell the compiler that, using a promise_equivalent_solutions
    scope. For example, if the computation returns a list, but you care
    only about the set of items in it, and not their order or their multiplicity,
    then [1, 2], [2, 1] and [1, 2, 2, 1] are equivalent, and it does not matter
    which one you get. The *reason* this is a bit tricky in practice is that
    (a) you have to have in your mind an "equality theory" that partitions
    the space of outputs in a set of partitions, so that all solutions in a partition
    are equivalent, and then (2) write the *rest* of the program in such a way
    that it actually produces the same output no matter which element
    from a given equivalence class you give it. Getting this right is up to you.
    The compiler does not know your equality theory, and therefore
    cannot help you. (Actually, even if it did know, helping would require
    a full fledged theorem prover.)

The compiler *can* help you if you write code that asks cc_multi/cc_nondet
code to generate more than one solution. If say p is cc_multi, while q is
semidet, then the conjunction "p, ..., ..., q" won't work, because if q fails,
execution would have to backtrack to p to ask it to generate a second
solution, but cc_multi/cc_nondet predicates cannot do that. However,
in such cases, the compiler will tell you where the error is.

>> but I can live with that. Basically I sat and wrote down some study goals
>> and then over the last 23 days (according to my project diary) I’ve been
>> poking and prodding the compiler by writing a `det` predicate and then
>> breaking it, unbreaking it etc etc.
>> 
>> In the last week I have made fantastic progress with my language project,
>> I look forward to compiler errors. It’s a FANTASTIC language as I always
>> knew it would turn out to be 
> 
> Yes, Mercury's the real thing. In comparison, languages like Java and Python
> look rather ridiculous. :) 

I have a file of interesting quotes I have gathered over the years, mostly
from usenet news groups (when they were still a thing). One, from probably
around a quarter of a century ago, is relevant here. It goes like this:

  Of course SML does have its weaknesses, but by comparison, a discussion of
  C++'s strengths and flaws always sounds like an argument about whether one
  should face north or east when one is sacrificing one's goat to the rain god.

>> Thanks again.
> 
> You're welcome.

Let me add a "you're welcome" from the Mercury team as well.

Zoltan.