error-handling - 伊德瑞斯 12 月 vs 也许

Question

用Dec可以表达什么样的东西而不是与 Maybe在 idris ?

或者换句话说:什么时候应该选择 Dec当 Maybe ?

Answer 1

我在 one recent question 的回答中谈到了这一点。 .
使用 Dec 有两个原因:

您想证明事情并从实现中获得更多保证。

您希望您的函数在有限的时间内运行。

关于 1 .为 Nat 考虑这个函数平等:

natEq : (n: Nat) -> (m: Nat) -> Maybe (n = m)
natEq Z Z = Just Refl
natEq Z (S k) = Nothing
natEq (S k) Z = Nothing
natEq (S k) (S j) = case natEq k j of
    Nothing   => Nothing
    Just Refl => Just Refl

您可以为此函数编写测试并查看它是否有效。但是编译器无法在编译时阻止您编写 Nothing在每种情况下。这样的函数仍然是可编译的。 Maybe是某种弱证明。这意味着，如果您返回 Just那么您就可以找到答案，我们很好，但是如果您返回 Nothing这不代表任何意思。你就是找不到答案。但是当你使用 Dec你不能只是返回 No .因为如果你回来 No这意味着您实际上可以证明没有答案。所以重写natEq进入 Dec作为程序员，您需要付出更多努力，但实现现在更加强大:

zeroNotSucc : (0 = S k) -> Void
zeroNotSucc Refl impossible

succNotZero : (S k = 0) -> Void
succNotZero Refl impossible

noNatEqRec : (contra : (k = j) -> Void) -> (S k = S j) -> Void
noNatEqRec contra Refl = contra Refl

natEqDec : (n: Nat) -> (m: Nat) -> Dec (n = m)
natEqDec Z Z = Yes Refl
natEqDec Z (S k) = No zeroNotSucc
natEqDec (S k) Z = No succNotZero
natEqDec (S k) (S j) = case natEqDec k j of
    Yes Refl  => Yes Refl
    No contra => No (noNatEqRec contra)

关于 2 . Dec代表可判定性。这意味着您可以返回 Dec仅适用于可判定问题，即可以在有限时间内解决的问题。您可以解决Nat在有限时间内相等，因为你最终会陷入 Z .但是对于一些困难的事情，比如检查是否给出了 String代表计算前 10 个素数的 Idris 程序，你不能。