[m-users.] Performance of solutions module

[Zoltan Somogyi]

On Tue, 6 Nov 2018 14:10:47 +0400, Fred Mesnard <frederic.mesnard at gmail.com> wrote:
> > Le 6 nov. 2018 à 02:10, Zoltan Somogyi <zoltan.somogyi at runbox.com> a écrit :
> > 
> > There are two kinds of semantics that are relevant here. One is the
> > declarative semantics: what a piece of code is supposed to mean.
> > The other is the operational semantics: what the compiled version
> > of that code actually does. Mercury is a declarative language
> > because in almost all cases, the compiler is required to ensure
> > that the operational semantics matches the declarative semantics.
> > 
> > Committed choice code is one of the main exceptions.
> 
> Thanks for the explanations you gave! 
> What are the other exceptions?

There are some obvious exceptions.

Anything involving a foreign language is an obvious exception.
The Mercury compiler cannot be expected to ensure that the declarative
and operational semantics match for predicates defined in a foreign language,
or for code using a type defined in a foreign language (since the values
of the foreign type are subject to manipulation not just by code generated
by the Mercury compiler, but by foreign language code as well).
If foreign language code has a declarative semantics, it is not accessible
to the Mercury compiler.

Anything involving impure or semipure code is also an obvious exception.
Most such code uses foreign language code, but there are some Mercury
constructs (mutables that are not attached to the I/O state)
that also introduce impurity. Code is marked impure or semipure,
and then wrapped up inside a promise_pure scope, precisely to tell
the compiler that it is the job of the programmer, not the compiler,
to make the declarative and operational semantics match.

There are several other promise constructs in Mercury that also
have this same job, but in different contexts. One such constructs
is the promise_equivalent_clauses pragma, which tells the compiler
that all the various mode-specific clauses of a predicate implement
the same declarative semantics. For example, a factorization predicate
could have one clause for the in,out mode where it returns a list of the
prime factors of the input integer, and another clause for the in,in mode
which simply checks that the integers listed in the second argument
(a) yield in the first argument when multiplied together, and (b) are
prime themselves. Much of cryptography depends on the fact that
the code of the second clause can be *many* orders of magnitude
faster than the first, using completely different code. No compiler
can be expected to prove such different pieces of code
to be equivalent, hence the need for the programmer's promise.

Zoltan.