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

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 the compiler says: "When you declared type test_case , you did not specify determinism, so I assumed that you had in mind det . But then you went into semidet lambda."

My questions:

• What is the syntax for declaring type determinism? Guesses I tried led to syntax errors.
• Can someone explain what the /* unique */ part of the <100> instance means? Will this cause a mismatch between this and the expected instance?
• Is there a less correct way to declare lambda in main ? I have the same lambda declaration as in lambda code.

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

It took me a while to hang too.

The problem is that a higher order mode is not part of its type. Thus, there is no syntax for declaring type determinism. Higher-order determinism is tolerated in mode.

In your example, the first argument to assert_equals is of type test_case(T) , but has a mode of in . This means that the semidet function is lost. I'm not sure if it will really compile or run correctly if the function you pass was det ; even in this case, the mode really should not be in .

Here is 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 this higher-order function takes one argument and returns a result of the same type. This is a mode declaration, which actually says that the parameter of the function has the mode in , and the result of the function has the mode out , and its determinism is det .

I believe that the /*unique */ bit of the error message says that the compiler considers it unique. I am not sure if this is a problem or not, since you are not using unique modes anywhere other than the normal io state.

Regarding lambda syntax, I don't think you can do anything for the better, unfortunately. I find the lambda syntax in Mercury to be quite unsatisfactory; they are so verbose that I usually end up doing named functions / predicates instead of all but the most trivial lambdas.

---

---

Answer 2

Ben is right

I would like to add that Mercury assumes that functions are deterministic by default (it is reasonable that functions must be deterministic). This is not true for predicates in which determinism must be declared. This simplifies higher order programming with deterministic functions than any other function or predicate, simply because there are fewer templates.

Because of this, you can make your lambda expression a bit more concise. You can also move the body of a lambda expression to the head by replacing the S variable in the head with the body.

 apply_transformer((func(S0) = "Hello " ++ S0), "World", Msg), 

Answer 3

To answer the second question, /* unique */ in the error message refers to the first argument to invoke assert_equals , which is the lambda term just created. This is the only place the term is used, so the link to it is unique at the point of call.

A unique inst corresponds to the main inst (but not vice versa), so in this case, uniqueness will not cause a mismatch. This is determinism, which is a problem.