Idris Dec与Maybe的区别

Question

Dec和Maybe在Idris中分别用来表达什么样的内容？

换句话说，何时应该选择使用Dec，何时应该选择使用Maybe？

- freddie-freeloader

---

也许你会发现阅读标准库中 isItJust : (v : Maybe a) -> Dec (IsJust v) 函数的定义很有帮助或者很有趣，该函数“决定一个 'Maybe' 是否为 'Just'”。 - Mekeor Melire

Answer 1

我在最近的一个问题中已经谈到了这个问题的一点。使用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程序，你就做不到了。

- Shersh