[m-users.] Functions vs Predicates?

Zoltan Somogyi zoltan.somogyi at runbox.com
Sat Oct 31 04:29:03 AEDT 2020


2020-10-31 04:01 GMT+11:00 "Qqwy/Wiebe-Marten" <qqwy at gmx.com>:
> I indeed got the experience from introductory Prolog texts (most notably
> Markus Triska's "The Power of Prolog")
> that creating predicates which retain as much "logical purity" as
> possible are beneficial to keep your code flexible and thus testable and
> maintainable. (c.f. https://www.metalevel.at/prolog/purity )/
> /Of course, whether this sentiment is (a) shared by more experienced
> Prolog developers, and (b) can be applied 1:1 to Mercury are things I do
> not know.
> 
> Could you elaborate on this?

I wouldn't presume to speak for Prolog developers, so I cannot address
part (a), but I can address part (b). For Mercury developers, this advice
is almost unnecessary, for a simple reason: with a few exceptions such as
the foreign language interface, the entire Mercury language enforces
logical purity. In Prolog, there are many things that you cannot do
using only pure code; this is not true for Mercury.

> A related question is about higher-order predicates/functions, such as
> `list.map`:
> 
> I tried to translate a Prolog Sudoku-solver/generator/tester (c.f.
> http://rosettacode.org/wiki/Sudoku#Prolog) to Mercuy, and immediately
> encountered
> the problem that higher-order predicates/functions such as `list.map`
> seemingly can only be used in a single mode at a time,
> since the predicate/function you pass to it needs to have only a single
> mode (if it has multiple you need to wrap it in a lambda expression that
> exposes only one of them).
> (C.f. the reference manual, 8.1)
> 
> Is this an implementation limitation that might be lifted some time in
> the future?
> Or is this an inherent limitation of logic-based type checking? (Would
> type-checking become undecidable if multiple modes are allowed?)
> Or maybe I am simply doing something wrong?

You misunderstand the nature of the problem. It has nothing to do with
list.map or other higher order constructs, but is more fundamental than that.
Mercury's mode system requires programs to have statically decidable data flow,
i.e. the compiler must be able to figure out which subgoals bind which variables.
For puzzle programs such as sudoku, this is not possible. It is possible
in Prolog only because Prolog has a builtin constraint solver for so-called
Herbrand constraints, which means a solver for arbitrary form unifications.
(Many Prolog dialects also have builtin solvers for other kinds of constraints,
but Herbrand constraints are the only ones in standard Prolog.)

The difference between unification in Prolog and Mercury is that given a
unification between e.g. two variables X and Y, Mercury can execute the unification
only when at least one of X and Y is ground, and the Mercury compiler needs to know
at compile time which variable this will be. By contrast, Prolog can execute
the unification even if both X and Y are free variables. This is more flexible,
but it also has costs. The most important cost is that such unifications,
while useful in puzzle programs, are often the sign of a bug in a very large
fraction of other kinds of programs. A less important cost is that having
to be ready to follow variable-to-variable bindings slows down pretty much
every operation in every Prolog program.

This difference is thus a consequence of the different priorities
of the designers of Prolog and Mercury.

So the answer to your question is: no, this limitation will not be
lifted in the future.

Zoltan.


More information about the users mailing list