":=" and "=>" in Mercury

I recently came across this code example in Mercury:

append开发者_运维知识库(X,Y,Z) :-
  X == [],
  Z := Y.
append(X,Y,Z) :-
  X => [H | T],
  append(T,Y,NT),
  Z <= [H | NT].

Being a Prolog programmer, I wonder: what's the difference between a normal unification = and the := or => which are use here?

In the Mercury reference, these operators get different priorities, but they don't explain the difference.

---

First let's re-write the code using indentation:

append(X, Y, Z) :-
    X == [],
    Z := Y.
append(X, Y, Z) :-
    X => [H | T],
    append(T, Y, NT),
    Z <= [H | NT].

You seem to have to indent all code by four spaces, which doesn't seem to work in comments, my comments above should be ignored (I'm not able to delete them).

The code above isn't real Mercury code, it is pseudo code. It doesn't make sense as real Mercury code because the <= and => operators are used for typeclasses (IIRC), not unification. Additionally, I haven't seen the := operator before, I'm not sure what is does.

In this style of pseudo code (I believe) that the author is trying to show that := is an assignment type of unification where X is assigned the value of Y. Similarly => is showing a deconstruction of X and <= is showing a construction of Z. Also == shows an equality test between X and the empty list. All of these operations are types of unification. The compiler knows which type of unification should be used for each mode of the predicate. For this code the mode that makes sense is append(in, in, out)

Mercury is different from Prolog in this respect, it knows which type of unification to use and therefore can generate more efficient code and ensure that the program is mode-correct.

One more thing, the real Mercury code for this pseudo code would be:

:- pred append(list(T)::in, list(T)::in, list(T)::out) is det.

append(X, Y, Z) :-
    X = [],
    Z = Y.
append(X, Y, Z) :-
    X = [H | T],
    append(T, Y, NT),
    Z = [H | NT].

Note that every unification is a = and a predicate and mode declaration has been added.

---

In concrete Mercury syntax the operator := is used for field updates.

---

Maybe we are not able to use such operators like ':=' '<=' '=>' '==' in recent Mercury release, but actually these operators are specialized unification, according to the description in Nancy Mazur's thesis. '=>' stands for deconstruction e.g. X => f(Y1, Y2, ..., Yn) where X is input and all Yn is output. It's semidet. '<=' is on the contrary, and is det. '==' is used in the situation where both sides are ground, and it is semidet. ':=' is just like regular assigning operator in any other language, and it's det. In older papers I even see that they use '==' instead of '=>' to perform a deconstruction. (I think my English is awful = x =)