Mercury: Determinism and pattern matching

Question

I have a semideterministic function. When I re-write it to use pattern matching instead of an if statement, Mercury says it becomes nondeterministic. I'd like to understand why.

The original code:

:- pred nth(list(T), int, T).
:- mode nth(in,      in,  out) is semidet.
nth([Hd | Tl], N, X) :- (if N = 0 then X = Hd else nth(Tl, N - 1, X)).

The revised code:

:- pred nth(list(T), int, T).
:- mode nth(in,      in,  out) is nondet.
nth([Hd | _], 0, Hd).                             % Case A
nth([_ | Tl], N, X) :- N \= 0, nth(Tl, N - 1, X). % Case B

I'm used to thinking about pattern matching in SML, where the 0 in case A would ensure that in case B, N is not 0. Does Mercury work differently? Could case B get called, even if N is 0? (I added the N \= 0 clause to case B in the hope of making the predicate semideterministic, but that didn't work.)

Is there a way writing this predicate with pattern matching that is also semideterministic?

Answer 1

Yes, Mercury pattern matching works differently to SML. Mercury is pretty strict about its declarative semantics. A predicate with multiple clauses is equivalent to a disjunction of all the bodies (modulo some complications for unifications in the clause heads), and the meaning of a disjunction is unaffected by the order in which the different arms of the disjunction are written. In fact very little of Mercury has its meaning affected by the order you write things (state variables are the only example I can think of).

So without putting N \= 0 in the body, your predicate with two clauses using pattern matching is nondeterministic. There would be nothing to stop nth(Tl, 0 - 1, X) being a valid reduction of nth([_ | Tl], 0, X).

With the N \= 0, you're getting on the right track. Unfortunately, while if A then B else C is logically equivalent to (A, B) ; (not A, C), Mercury's determinism inference isn't usually smart enough to figure out the reverse.

In particular, Mercury's determinism inference doesn't attempt to figure out in general that two clauses are mutually exclusive. In this case, it knows that N = 0 can succeed or fail, depending on the value of N, and that N \= 0 can suceed or fail, depending on the value of N. Since it sees two different ways for the predicate to succeed, and it can fail, it must be nondeterministic. There are ways to promise to the compiler that the detminism isn't what it would infer, but in cases like this it's easier to just stick to using if/then/else.

The cases where you can use pattern matching without the compiler thinking you can have multiple solutions are when you are matching a single variable against several different constructors of the same type. For example:

:- pred some_pred(list[T]) is det.
some_pred([]) :- something.
some_pred([H | T]) :- something_else.

This is called a switch. The compiler knows that a list has two constructors (the empty list [], or the cons cell [|]), and a given list can only be one of those, so a disjunction (or multiple clauses of a predicate) that has an arm for both constructors must be deterministic. A disjunction (multiple clauses) with cases for some but not all of the constructors will be inferred as semi-deterministic.

Mercury is also able to generate very efficient code for switches, and also notify you of all the places that need changing when you change a type by adding new cases, so it is considered good style to use switches where possible. In cases like yours however, you're stuck with if/then/else.