[m-users.] A more precise determinism checker

[Philip White]

Thanks for all your comments everyone. As usual the discussion on this
list is high quality.

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. 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.

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.

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.

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.

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. 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.

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.

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