伊德里斯 12 月 VS 可能

Question

Idris中的Dec而不是Maybe可以表达什么？

或者换句话说：什么时候应该选择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 程序，你不能。