Idris Dec vs Maybe

Question

What kind of things can one express with Dec and not with Maybe in Idris?

Or in other words: When should one choose Dec and when Maybe?

Answer 1

I told a little bit about this in the answer to the one recent question. There're two reasons for using Dec:

1. You want to prove things and have more guarantees from the implementation.
2. You want your function to run in finite time.

Regarding 1. Consider this function for Nat equality:

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

You can write tests for this function and see if it works. But compiler can't stop you at compile-time from writing Nothing in every case. Such function still will be compilable. Maybe is some sort of weak proof. It means, if you return Just then you're able to find answer and we are good but if you return Nothing it means nothing. You just can't find answer. But when you're using Dec you can't just return No. Because if you're returning No it means that you can actually prove that there is no answer. So rewriting natEq into Dec will require more effort from you as a programmer but implementation is now more robust:

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)

Regarding 2. Dec stands for decidability. It means that you can return Dec only for decidable problems, i.e. problems that can be solved in finite time. You can solve Nat equality in finite time because you'll eventually fall into case with Z. But for something difficult, like, check whether given String represents Idris program that calculates first 10 prime numbers, you can't.