First, let’s try to understand what Idris’s Refl does. It is defined as such:
data (=) : a -> b -> Type where
Refl : x = x
Now, let’s try to implement nats ourselves:
data MyNat = Zero | Next MyNat my_add : MyNat -> MyNat -> MyNat my_add Zero m = m my_add (Next k) m = Next (my_add k m)
What Idris does here at compile time, when it sees Refl it tries to evaluate the values by the given definitions. So it understands that (0 + 1) = 1, by my_add and definition of MyNat. E.g.:
my_proof : my_add Zero (Next Zero) = Next Zero my_proof = Refl
Now let’s try to write functions (both head and tail recursive) that will convert a list to a vector so we have the length of the list at type level.
data Vect : Nat -> Type -> Type where VNil : Vect Z a VCons : a -> Vect k a -> Vect (S k) a
We will prove watwat with the following type. We’ll see how and why we’ll be using it later.
watwat : (left : Nat) -> (right : Nat) -> S (plus left right) = plus left (S right) watwat Z right = Refl -- to prove S (plus 0 right) = plus 0 (S right) it's just reflexivity, by def of plus
Now for the other case (first argument not zero), if we write a hole:
watwat (S left) right = ?hole
and check what we need to fill in: hole : S (S (plus left right)) = S (plus left (S right))
So in theory, we need to pass a lambda function which will take values from the previous type and produce values to match the new type.
That is, what we need to show here is that we can go from
S (plus left right) = plus left (S right)
to
S (plus (S left) right) = plus (S left) (S right) [original definition],
i.e. S (S (plus left right)) = S (plus left (S right)) [simplified by Idris when we checked the hole].
So now, it’d be good if we had a function with type (a = b) -> f a = f b. So we could’ve just used it with (watwat left right) to get the correct match. Core already has cong and it is exactly what we need.
watwat (S left) right = cong (watwat left right)
We proved it using lambda terms. To prove it with tactics, equivalently:
watwat (S left) right =
let inductiveHypothesis = watwat left right in
rewrite inductiveHypothesis in Refl
-- Or, even simpler, just watwat = plusSuccRightSucc
Now let’s go ahead and implement a function that converts a list to a vector (the vector will know the length at type level):
-- The following head recursion works fine, because types flow nicely f : (l : List Char) -> Vect (length l) Char f [] = VNil f (x :: xs) = VCons x (f xs)
Now let’s implement the tail recursion of the same computation
f_tail : Vect n Char -> (l : List Char) -> Vect (length l + n) Char f_tail v [] = v
The following won’t work because types won’t match:
f_tail {n} v (x :: xs) = f_tail (VCons x v) xs
If, instead we use a hole:
f_tail {n} v (x :: xs) = ?hole
We get that hole : Vect (S (plus (length xs) n)) Char
So we need to go from
Vect (length xs + S n) Char (Type of f_tail (VCons x v) xs)
to
Vect (S (plus (length xs) n)) Char (Expected type).
We can use our watwat theorem to get to it.
f_tail {n} v (x :: xs) =
let inductiveHypothesis = watwat (length xs) n in
rewrite inductiveHypothesis in (f_tail (VCons x v) xs)
To implement this in lambda terms, we first introduce ourselves to replace and sym:
*induction> :t replace replace : (x = y) -> P x -> P y *induction> :t sym sym : (left = right) -> right = left *induction>
Example usage:
f : 3 = (4 - 1) f = Refl
Now note how Idris evaluates the types:
*test> :t replace
replace : (x = y) -> P x -> P y
*test> :t replace {f = \x => Vect x Char} f
cong f : Vect 3 Char = Vect 3 Char
So proceeding with our implementation in lambda terms:
f_tail {n} v (x :: xs) =
f_tail {n} v (x :: xs) = replace {P = \m => Vect m Char} (sym (watwat (length xs) n)) (f_tail_l (VCons x v) xs)
To recap what we did, by Curry-Howard isomorphism (proof by lambda construction) we proved the following theorems:
(left : Nat) -> (right : Nat) -> S (plus left right) = plus left (S right) (l : List Char) -> Vect (length l) Char Vect n Char -> (l : List Char) -> Vect (length l + n) Char
Bonus:
We can use :set showimplicits to see the implicit arguments, so that we can pass stuff to them.
Given:
f : 3 = 3 f = Refl
Here’s an example of cong which doubles an equality:
double : (x = x) -> (x + x = x + x)
double n = cong {f = \x => x + x} n
And another example of replace which replaces the type:
test_replace : {n : Type} -> (x = x) -> n -> n
test_replace f = replace {P = \x => n} f
Results in:
*test> double f
Refl : 6 = 6
*test> test_replace {n = Bool} f
replace Refl : Bool -> Bool
bor0's reflective blog 