Свойства ADT в Mercury

Я не понимаю, почему Mercury (10.04) не может вывести детерминизм следующего фрагмента:

:- pred load_freqs(int::in, io.res(list(float))::out, io::di, io::uo) is det.
load_freqs(CPU, ResFreqs, !IO):-
    open_input(cpu_fn(CPU, "available_frequencies"), ResStream, !IO),
    (ResStream = io.ok(Stream) ->
        ResFreqs = io.ok([])
    ;ResStream = io.error(Err),
        ResFreqs = io.error(Err)
    ).

Он жалуется:

cpugear.m:075: In `load_freqs'(in, out, di, uo):
cpugear.m:075:   error: determinism declaration not satisfied.
cpugear.m:075:   Declared `det', inferred `semidet'.
cpugear.m:080:   Unification of `ResStream' and `io.error(Err)' can fail.
cpugear.m:076: In clause for predicate `cpugear.load_freqs'/4:
cpugear.m:076:   warning: variable `CPU' occurs only once in this scope.
cpugear.m:078: In clause for predicate `cpugear.load_freqs'/4:
cpugear.m:078:   warning: variable `Stream' occurs only once in this scope.

Но у io.res есть только io.ok/1 и io.error/1.
Следующий фрагмент кода компилируется хорошо:

:- pred read_freqs(io.res(io.input_stream)::in, io.res(list(float))::out, io::di, io::uo) is det.
read_freqs(io.ok(Stream), io.ok([]), IO, IO).
read_freqs(io.error(Err), io.error(Err), IO, IO).

Обновление №1: оно может решить даже для:

:- pred read_freqs(bool::in, io.res(io.input_stream)::in, io.res(list(float))::out, io::di, io::uo) is det.
read_freqs(no, ResStream, io.ok([]), IO, IO):- ResStream = io.ok(_).
read_freqs(F, io.ok(_), io.ok([]), IO, IO):- F = yes.
read_freqs(yes, io.error(Err), io.error(Err), IO, IO).
read_freqs(F, ResStream, io.error(Err), IO, IO):- ResStream = io.error(Err), F = no.

logic declarative mercury
person ony    schedule 29.07.2010    source источник

Ответы (3)


arrow_upward
2
arrow_downward

Мое прочтение правил Mercury для детерминизма с условными выражениями (ниже) заключается в том, что для того, чтобы это считалось детерминированным, вы должны заменить -> на ,

Из справочного руководства Mercury:

Если условие «если-то-иначе» не может нарушиться, то «если-то-иначе» эквивалентно соединению условия и части «тогда», и соответственно вычисляется его детерминизм. В противном случае оператор if-then-else может потерпеть неудачу, если либо часть «тогда», либо часть «иначе» могут завершиться ошибкой.

person RD1    schedule 29.07.2010
comment
В этом случае ResStream может объединяться с io.ok(Stream), но также может объединяться с io.error(Err). Это зависит от результата открытия файла. Для этого есть две ветки. Чтобы получить эксклюзив или я использую конструкцию if-the-else, и, как согласно вашей цитате, она должна подойти. Но Меркьюри не может сделать вывод, что not(ResStream = ok(_)) => ResStream = error(_). - person ony; 29.07.2010
comment
В вашем случае ветвь else — это ResStream = io.error(Err), ResFreqs = io.error(Err), которая завершится ошибкой, если ResStream — это io.ok(X). Процитированное мною правило ничего не говорит о добавлении отрицания условия. Я согласен, что логически это можно было бы добавить, но в справочнике указано, что это не так. Напротив, дизъюнкции рассматриваются особым образом, если они имеют форму переключателя, что, по-видимому, допускает конъюнкции в дизъюнкциях, но не в условных предложениях. Я предполагаю, что причина в том, что в общем случае шаблоны не пересекаются, и в этом случае и -> делают то же самое. - person RD1; 29.07.2010
comment
Узоры могут пересекаться, и Меркурий находит эти пересечения, делая вывод о множественном детерминизме. См. дополнительный пример. Если вы решите дет. только по голове, чем read_freqs (в обновлении) будет помечен как мульти. - person ony; 30.07.2010

arrow_upward
2
arrow_downward

Что касается «почему». давайте посмотрим на исходный код с if-then-else:

(ResStream = io.ok(Stream) ->
    ResFreqs = io.ok([])
;ResStream = io.error(Err),
    ResFreqs = io.error(Err)
).

Если условие не выполняется, то первый конъюнкт в случае else является тестом semidet. Компилятор не знает, что он должен завершиться успешно (что можно сделать, зная, что это условие не выполнено). Другими словами, компилятор недостаточно умен.

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

По возможности рекомендуется программировать с использованием переключателей (например, в этом примере), это предотвращает текущую проблему и помогает гарантировать, что вы охватили все возможные случаи ResStream. Например, если в будущем io.error подвергнется рефакторингу и может быть io.error_file_not_found или io.error_disk_full и т. д., компилятор направит программиста на исправление своего переключателя, так как теперь он будет неполным.

person Paul Bone    schedule 07.02.2011
comment
На данный момент мне проще понять, что через (X = yes, true; not(X = yes), X = no) (это то, что я ожидаю от (X = yes -> true; X = no)) будет выводиться в nondet из-за not/1. - person ony; 07.02.2011
comment
Это верно до тех пор, пока условие не станет более сложным. Если либо символов больше, чем да или нет, либо в условии более одного объединения. - person Paul Bone; 09.02.2011

arrow_upward
1
arrow_downward

Хорошо, он может вывести det для:

:- pred load_freqs(int::in, io.res(list(float))::out, io::di, io::uo) is det.
load_freqs(CPU, ResFreqs, !IO):-
    open_input(cpu_fn(0, "available_frequencies"), ResStream, !IO),
    (ResStream = io.ok(Stream),
        ResFreqs = io.ok([])
    ;ResStream = io.error(Err),
        ResFreqs = io.error(Err)
    ).

Но почему конструкция «если-то-иначе» вводит семидет?

person ony    schedule 30.07.2010
comment
Мой первый ответ почему? это потому, что это то, что говорится в справочном руководстве Mercury. Но, я думаю, вы имеете в виду, почему Mercury спроектирован именно так? Я предполагаю, что к переключателям нужно относиться по-особому, и дизайнеры не хотели делать их более сложными, чем необходимо, а избегание негативной информации действительно упрощает дело. Кроме того, у меня сложилось впечатление, что Меркьюри обычно поощряет переключатели, а не условные выражения. Действительно, есть переключатель --inform-ite-instead-of-switch, позволяющий сообщать об условных выражениях, которые следует заменить переключателями. - person RD1; 30.07.2010
comment
Спасибо, полезная опция --inform-ite-instead-of-switch. - person ony; 30.07.2010