Idris Dec vs Maybe

I've talked a little about this in response to a recent question . There are two reasons for using Dec

:

• You want to prove things and get more guarantees from the implementation.
• You want your function to execute in finite time.

Relative to 1 . Consider this function for equality 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

      

        
        
        
      

    

You can write tests for this function and see if it works. But the compiler cannot stop you at compile time by writing Nothing

in every case. Such a function will still be compiled. Maybe

is kind of weak evidence. This means that if you come back Just

then you can find the answer and we are good, but if you come back Nothing

it means nothing. You just can't find the answer. But when you use Dec

, you cannot just return No

. Because if you return No

it means that you can actually prove there is no answer. Therefore, rewriting natEq

in Dec

will require more effort from you as a programmer, but the implementation is now more reliable:

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)

      

        
        
        
      

    

Relatively 2 . Dec

means solvability. This means that you can Dec

only return for solvable problems, that is, problems that can be resolved in a finite time. You can solve the equality Nat

in finite time because you will eventually get into a deal with Z

. But for something tricky like check if the given String

program matches Idris which calculates the first 10 primes, you can't.