Меркурий: Как объявить детерминизм типа данных более высокого порядка?

Когда я компилирую код Mercury ниже, я получаю эту ошибку от компилятора:

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)'.

Я думаю, что компилятор говорит: "Когда вы объявили тип test_case, вы не указали детерминизм, поэтому я предположил, что вы имели в виду det, Но потом вы прошли в semidet лямбда ".

Мои вопросы:

  • Какой синтаксис для объявления детерминизма типа? Все предположения, которые я попробовал, привели к синтаксическим ошибкам.
  • Может кто-нибудь объяснить, что /* unique */ часть TestCaseинстанцированность означает? Приведет ли это к несоответствию между данной и ожидаемой инстанцированностью?
  • Есть ли менее подробный способ объявления лямбды в main? У меня столько же объявлений о лямбде, сколько и кода внутри лямбды.

Код:

% (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).
Источник

3 ответа

Решение

Это заняло у меня некоторое время, чтобы овладеть также.

Проблема в том, что мода члена более высокого порядка не является частью его типа. Таким образом, нет синтаксиса для объявления детерминизма типа. Детерминизм члена более высокого порядка осуществляется в моде.

В вашем примере первый аргумент assert_equals имеет тип test_case(T), но имеет режим in, Это означает, что тот факт, что функция semidet теряется Я не уверен, что он действительно скомпилируется или будет работать правильно, если передаваемая вами функция была det; даже в этом случае режим действительно не должен быть in,

Вот пример:

:- 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).

Как видите, тип первого аргумента apply_transformer Только говорит, что это функция высшего порядка, принимает один аргумент и возвращает результат того же типа. Это объявление режима, которое на самом деле говорит, что параметр функции имеет режим in и результат функции имеет режим outи что его детерминизм det,

Я верю /*unique */ бит сообщения об ошибке говорит о том, что компилятор считает, что это уникальное значение. Я не уверен, является ли это проблемой или нет, так как вы не используете уникальные режимы где-либо, кроме обычного io государство.

Что касается лямбда-синтаксиса, я не думаю, что вы можете добиться большего успеха, к сожалению. Я нахожу синтаксис лямбд в Меркурии довольно неудовлетворительным; они настолько многословны, что я обычно просто делаю именованные функции / предикаты вместо всех, кроме самых тривиальных лямбд.

Источник

Бен прав,

Я хотел бы добавить, что Меркурий предполагает, что функции являются детерминированными по умолчанию (разумно, чтобы функции были детерминированными). Это не верно для предикатов, в которых детерминизм должен быть объявлен. Это облегчает программирование более высокого порядка с детерминированными функциями, чем любая другая функция или предикат, просто потому, что здесь меньше шаблонов.

Благодаря этому вы можете сделать свое лямбда-выражение немного более лаконичным. Вы также можете переместить тело лямбда-выражения в голову, подставив в голову переменную S в голове.

apply_transformer((func(S0) = "Hello " ++ S0),
                  "World", Msg),
Источник

Чтобы ответить на второй вопрос, /* unique */ в сообщении об ошибке ссылается на первый аргумент вызова assert_equals, который является лямбда-термином, который вы только что создали. Это единственное место, где используется термин, поэтому ссылка на него уникальна в момент вызова.

Уникальный экземпляр соответствует базовому (но не наоборот), поэтому в этом случае уникальность не приведет к несоответствию. Проблема в детерминизме.

Источник
Другие вопросы по тегам