Idris Dec诉也许

Question

一个人能用Dec而不是Maybe在Idris上表达什么样的东西？

或者换句话说:何时选择Dec，何时选择Maybe

Answer 1

我在one recent question的答案中提到了这一点。使用Dec有两个原因

1. 您想要证明一些事情，并从实现中获得更多的保证。
2. 你想让你的函数在有限的时间内运行。

关于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程序，你不能。