Idris Dec vs Maybe

Question

一个可以表达什么样的事情Dec,而不是用Maybe在伊德里斯？

换句话说:什么时候应该选择Dec什么时候Maybe？

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程序,你不能.