[m-users.] A more precise determinism checker

[Philip White]

Hi Folks,

I've been working in my spare time on a compiler for a relational
programming language heavily inspired by mercury - it has strong and
statically checked types, modes, and determinism.

The determinism checking approach of this language is totally different
than Mercury's approach, and I believe it yields much more precise
results, albeit via a more expensive algorithm. I'm curious if the
compiler writers ever considered something like this. If not, would you
every consider using it in the current mMrcury compiler?

Predicates written in this language go through a mode-resolution phase
in which clauses in a conjunction are re-ordered so that variables are
properly instantiated for each predicate that needs to be invoked; this
phase also selects the mode to use at each invocation. It's after this
phase that I run the determinism checker. I imagine the Mercury
compiler does something pretty similar.

Determinism inference receives a mode-resolved predicate as input and
produces a determinism (the possible determinisms are the same as in
Mercury).

The algorithm first collects a mapping from each variable to the
possible constructors for that variable; variables that are outputs of
predicate invocations get mapped to the set of all constructors of
their type, for example.

Naively, we "execute" the predicate with each combination of
constructors that each variable can have. This guarantees that we will
hit every possible code-path of the predicate. The result of each
execution is a determinism. For example, if the predicate finishes
twice, then the result of that execution is "multi". The final
determinism of the predicate is the join of all the execution results
(i.e. the join operation of the determinism lattice). For example, if
one path yields "multi" and another yields "failure", then the final
determinism is "nondet".

This naive approach would be prohibitively expensive for predicates
with lots variables, especially if those variables have types with many
constructors. We can improve it by initially treating every variable as
abstract; every time the predicate attempts to pattern match a
variable, we restart execution once for each of that variable's
constructors. The algorithm is roughly the same, but we only end up
running variable combinations on-demand, so we save a lot of work
for variables that are merely moved around and never inspected.

There are a few details that I've glossed over, but this is the general
idea. It's definitely a more expensive algorithm than something that is
more syntax directed, but I think it will notice switch statements more
often than Mercury does, and it will also determine that a set of
variables is exhaustive more often than the Mercury compiler. (I make
this claim mostly based on my understanding of the Mercury compiler
from the documentation, rather than from experience; I bet I can
furnish examples if you would like to see any, though)

I'd love to hear what people think of this approach. I haven't yet
tested it at large scale with huge predicates, so my biggest concern is
that it will be really, really slow.

- Philip