The Author Online Book Forums are Moving

The Author Online Book Forums will soon redirect to Manning's liveBook and liveVideo. All book forum content will migrate to liveBook's discussion forum and all video forum content will migrate to liveVideo. Log in to liveBook or liveVideo with your Manning credentials to join the discussion!

Thank you for your engagement in the AoF over the years! We look forward to offering you a more enhanced forum experience.

xoltar (3) [Avatar] Offline
Around p. 248 in v9, we're talking about equality, and cong. After this section, I have two questions:

checkEqNat : (num1 : Nat) -> (num2: Nat) -> Maybe (num1 = num2)
checkEqNat Z Z = Just (Refl)
checkEqNat Z (S k) = Nothing
checkEqNat (S k) Z = Nothing
checkEqNat (S k) (S j) = do
           prf <- checkEqNat k j
           pure (cong prf)

exactLength : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
exactLength {m} len input = do
            Refl <- checkEqNat m len
            pure input

1. Why do we have to pattern match in exactLength? Why isn't
prf <- checkEqNat m len
2. It seems like the function that cong is using as its implicit argument in checkEqNat is S. So why doesn't the following work?

??> the (S 3 = S 3) (cong (the (3=3) Refl))
(input):1:5:When checking argument value to function Prelude.Basics.the:
        Type mismatch between
                f 3 = f 3 (Type of cong (the (3 = 3) Refl))
                S 3 = S 3 (Expected type)
                Type mismatch between
                        f 3

Edwin Brady (66) [Avatar] Offline
1. Even though Refl is the only constructor for =, the type checker needs to know that when you run checkEqNat it really does return Refl. If checkEqNat isn't total, for example, it might not return anything at all.

2. Idris is more careful about inferring values of implicit arguments of function types, because in general there could be any number of functions which match. Here, for example, another function which could match might be something like:

other : Nat -> Nat
other x = if x < 10 then S x else S (S x)

So here, you need to be explicit since Idris won't work it out on its own