Mercury: How to declare determinism of a higher-order data type?

Question

When I compile the Mercury code below, I get this error from the compiler:

In clause for `main(di, uo)':
  in argument 1 of call to predicate
  `test_with_anonymous_functions.assert_equals'/5:
  mode error: variable `V_15' has
  instantiatedness `/* unique */((func) =
  (free >> ground) is semidet)',
  expected instantiatedness was `((func) =
  (free >> ground) is det)'.

I think what the compiler is saying is "When you declared the type test_case, you didn't specify a determinism, so I assumed you meant det. But then you passed in a semidet lambda."

My questions:

• What's the syntax for declaring the determinism of a type? The guesses I've tried have all resulted in syntax errors.
• Can someone explain what the /* unique */ part of TestCase's instantiatedness means? Will that cause a mismatch, between the given & expected instantiatedness?
• Is there a less verbose way of declaring the lambda in main? I have as much declaration about the lambda as I do code inside the lambda.

The code:

% (Boilerplate statements at the top are omitted.)

% Return the nth item of a list
:- func nth(list(T), int) = T.
:- mode nth(in,      in)  = out is semidet.
nth([Hd | Tl], N) = (if N = 0 then Hd else nth(Tl, N - 1)).

% Unit testing: Execute TestCase to get the 
% actual value. Print a message if (a) the lambda fails
% or (b) the actual value isn't the expected value.
:- type test_case(T) == ((func) = T).
:- pred assert_equals(test_case(T), T,  string, io.state, io.state).
:- mode assert_equals(in,           in, in,     di,       uo) is det.
assert_equals(TestCase, Expected, Message, !IO) :-
    if   Actual = apply(TestCase), Actual = Expected
    then true % test passed. do nothing.
    else io.format("Fail:\t%s\n", [s(Message)], !IO).

main(!IO) :-
    List = [1, 2, 3, 4],
    assert_equals( ((func) = (nth(List, 0)::out) is semidet),
                 1, "Nth", !IO).

Answer 1

This took me a while to get the hang of as well.

The problem is that the mode of a higher-order term is not part of its type. So there is no syntax for declaring the determinism of a type. The determinism of a higher-order term is carried in the mode.

In your example, the first argument of assert_equals has type test_case(T), but has mode in. This means that the fact that the function is semidet gets lost. I'm not sure if it would actually compile or run correctly if the function you're passing was det; even in that case the mode really shouldn't be in.

Here's an example:

:- pred apply_transformer(func(T) = T, T, T).
:- mode apply_transformer(func(in) = out is det, in, out).
apply_transformer(F, X0, X) :-
    X = F(X0).

main(!IO) :-
    apply_transformer((func(S0) = S is det :- S = "Hello " ++ S0),
                      "World", Msg),
    print(Msg, !IO),
    nl(!IO).

As you can see, the type of the first argument to apply_transformer only says that it is a higher-order function takes one argument and returns a result of the same type. It's the mode declaration that actually says the function parameter has mode in and the function result has mode out, and that its determinism is det.

I believe the /*unique */ bit of the error message says that the compiler thinks it is a unique value. I'm not sure whether that's a problem or not, since you're not using unique modes anywhere other than the usual io state.

As for the lambda syntax, I don't think you can do any better unfortunately. I find the syntax of lambdas in Mercury to be fairly unsatisfactory; they're so verbose that I usually end up just making named functions/predicates instead for all but the most trivial lambdas.

---

---