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

Когда я компилирую приведенный ниже код 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).

lambda non-deterministic mercury
person Evan    schedule 11.09.2011    source источник

Ответы (3)


arrow_upward
3
arrow_downward

Мне тоже потребовалось некоторое время, чтобы освоиться.

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

В вашем примере первый аргумент 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.

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

person Ben    schedule 12.09.2011
comment
Спасибо, Бен. Это объяснение имеет смысл (и оно решило мою проблему!) - person Evan; 13.09.2011
comment
@Evan: я забыл добавить к своему ответу, также можно создавать псевдонимы режимов для сложных режимов терминов более высокого порядка. Однажды я сделал это для модуля с десятками предикатов, принимающих аргументы более высокого порядка одного и того же типа; Я объявил тип и режим в верхней части модуля и просто использовал их повсюду. - person Ben; 13.09.2011
comment
@Evan: эй, не могли бы вы взглянуть на stackoverflow.com/questions/13896296/ -- ничего общего с этим постом, просто для привлечения внимания к Эвану - person Dieter; 16.12.2012

arrow_upward
4
arrow_downward

Бен прав,

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

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

apply_transformer((func(S0) = "Hello " ++ S0),
                  "World", Msg),
person Paul Bone    schedule 12.09.2011

arrow_upward
2
arrow_downward

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

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

person Mark Brown    schedule 05.10.2014