Функция возвращает «Нет решения» вместо «Ничего»

Question

У меня есть стандартный тип данных, представляющий формулы логики предикатов. Функция, представляющая естественное правило исключения для дизъюнкции, может выглядеть следующим образом:

d_el p q =
  if p =: (Dis r s) && q =: (Neg r) then Just s else
  if q =: (Dis r s) && p =: (Neg r) then Just s else
     Nothing where r,s free

x =: y = (x =:= y) == success

Вместо оценки Nothing при сбое объединения, функция не возвращает решений в PACKS:

logic> d_el (Dis Bot Top) (Not Bot)
Result: Just Top
More Solutions? [Y(es)/n(o)/a(ll)] n
logic> d_el (Dis Bot Top) (Not Top)
No more solutions.

Чего мне не хватает, и почему el не оценивается как Nothing при сбое объединения?

Answer 1

Кажется, что это не лучший способ использовать эквациональные ограничения. Когда a =:= b терпит неудачу, тогда также завершается условие завершения функции.
E.g.:

xx x = if (x =:= 5) == success then 1 else x
xx x = 3

Оценка xx 7 приводит к 3 (не 7), потому что 7 =:= 5 полностью завершает первое предложение функции xx.

Я думаю, что код должен выглядеть следующим образом:

d_el p q = case (p,q) of
   (Dis a s, Neg b) -> if a == b then Just s else Nothing
   (Neg a, Dis b s) -> if a == b then Just s else Nothing
   _ -> Nothing