[m-users.] A more precise determinism checker

[Zoltan Somogyi]

2022-03-22 12:35 GMT+11:00 "Philip White" <philip at pswhite.org>:
> For some reason I was under the impression that Mercury would not do
> exhaustiveness analysis on multiple variables, which was one of the
> things that drove me to try this different approach. After trying to
> give some examples, I realized that this was incorrect.

While Prolog systems have traditionally only did indexing on
the top function symbol of the first argument of a predicate,
Mercury's approach to determinism analysis, from the beginning
of the project, has been to break out of these limitations. This meant

- indexing on the value of any variable, whether or not it is an argument;
- indexing on more than one variable; and
- indexing on more than function symbol position in a variable.

Basically, as long as there was a disjunction in which different disjuncts
unified the same part of the same variable with different function symbols,
we indexed on that part of that variable.

> I still think
> that my algorithm will do track more information and therefore yield
> more precise determinisms in certain cases, such as the if-then-else
> example that Zoltan gave. However, I'm guessing that Mercury does as
> well as OCaml or Haskell for exhaustiveness checking; I guess it does
> better because it also detects overlapping cases.

I am not up-to-date enough on the current state of either OCaml or Haskell,
but I do know that there were long stretches of time (years) when
our determinism analysis was more precise than theirs.

> The performance of the algorithm isn't unimportant to me, but it's not
> my main focus. It seems a shame to me for the compiler to not provide
> something to the programmer that it very well could. My goal with this
> compiler is to explore that as far as possible; for example, I also
> want to provide type-driven editing commands a la Idris and Agda, which
> provide tools for case splitting on variables and other stuff.

I have not heard of this before, but now I have a list of papers on it to read.
Thanks.
 
> If the determinism inference sounds too slow to you, you'll be
> horrified to learn that I'm currently also doing mode inference as
> well. I'm just doing a brute force search through all combinations of
> parameter modes to see which ones have a valid clause ordering. I need
> to find a way to trim some of these branches because it takes way too
> long to finish.

I don't whether you know that the Mercury compiler actually includes
a never-completed experimental mode analysis algorithm that
represents the problem that mode analysis needs to solve as a set
of constraints, and then tries to use ROBDDs (reduced ordered binary
decision diagrams) to solve them. The first part (representation) worked;
the second part (solving) did not, not well enough. Operations on ROBDDs
can be fast enough, but their worst case complexity is exponential in the
number of variables involved, and the PhD student working on it, David
Overton, did not find a way to guarantee the avoidance of such worst cases.
You can find a paper, a talk and David's thesis on this at

https://mercurylang.org/documentation/papers.html

(The option to enable this pass is --mode-constraints. It prints stuff,
but otherwise does not affect the compilation.)

Based on what I know now about constraint programming, I think an
approach based on constraint propagation has a chance of solving
mode analysis constraint systems fast enough to be practical.
However, to the best of my knowledge, noone has demonstrated
that yet.

> Thanks for the tip about concolic execution. It sounds a lot like what
> my approach has been, so I'll definitely have to look at the literature
> in that area to see if I'm just poorly reinventing what other people
> have been refining for years.

There has not a lot of work on determinism analysis recently
(since the concept of determinism does not exist an most languages),
but determinism analysis is program analysis, and that broader topic
has been an active research area since the 1950s, with lots of new ideas
in the last couple of decades. I would be surprised if concolic testing
was the *only* new idea relevant to determinism analysis.

> The concern about the algorithm being confusing is important. I think I
> can make the error messages quite clear however. The goal is to provide
> a justification for the inferred determinism.

Agreed. The Mercury compiler tries hard to present the justification
for every determinism error it reports.

> Even if the inferred
> determinism matches what was declared, it still would be nice to have
> an editor facility for asking the reasoning for why the determinism is
> correct.

Maybe. I think that would only be useful if it took the programmer
less time to type in the question than to derive the answer in his/her own head.
With a simple-enough determinism analysis algorithm, the latter
would almost always win, at least for experienced programmers.

> The justification of a determinism requires justifying both the lower
> and upper bound of solutions. For example, if the predicate can fail,
> the justification should show both the combinations of variables
> constructors that would trigger the failure as well as the position in
> the predicate that failure occurs. If the predicate could return
> multiple solutions, then the justification should also show the
> combination of variables that would succeed multiple times as well as
> the positions in the predicate that it could possibly succeed. I think
> an error like this, if presented well, would be easy to read and
> understand.

Agreed, but then, I think Mercury's current error messages
exhibit these properties already. (In the rare case when they don't,
my usual reaction is to modify the compiler to improve the error message,
sometimes without first  finishing whatever I was working when encountering
the insufficiently-helpful error message.)

> Anyway, I'm not really trying to convince you that you're wrong or that
> you should add this to Mercury.

I am open to new ideas, but the design parameters of Mercury are backed
by large amounts of practical experience, so the threshold that new ideas
have to improve upon is rather high. Nevertheless, new features *do* get
added to Mercury; see e.g. the recent addition of subtypes.

Zoltan.