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

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

4 голосов
/ 11 сентября 2011

Когда я компилирую код 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 ]

4 голосов
/ 12 сентября 2011

Бен прав,

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

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

apply_transformer((func(S0) = "Hello " ++ S0),
                  "World", Msg),
3 голосов
/ 12 сентября 2011

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

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

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

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

2 голосов
/ 05 октября 2014

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

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

...