函数返回“No Solution”而不是“Nothing”答案

【问题标题】：Function Returns "No Solution" Instead Of "Nothing"函数返回“No Solution”而不是“Nothing”
【发布时间】：2011-09-30 13:55:44
【问题描述】：

我有一个表示谓词逻辑公式的标准数据类型。表示析取的自然演绎消除规则的函数可能如下所示：

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？

【问题讨论】：

我使用的语言是 Curry，一种功能逻辑编程语言（见标签）。
哦 - 对不起....无知会很尴尬....
您可能知道，“咖喱”在其他语言（显然是 Haskell）中也是一个有意义的术语，所以也许您应该 add some content to the Stack Overflow wiki page for the curry tag。

标签： functional-programming logic-programming maybe curry

【解决方案1】：

这似乎不是使用等式约束的最佳方式。当a =:= b 失败时，完整的函数子句也会失败。
例如：

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

【讨论】：