Experimenting with cong in the Idris REPL

Question

TL;DR: I'd like an example or two of using cong in the Idris REPL to help me understand it better.

The generic equality type is conceptually defined like so:

data (=) : a -> b -> Type where
  Refl : x = x

When I first encountered this, I was very confused by the syntax. (I kept thinking of = as an operator rather than a type.) But playing around with it in the REPL helped me to understand. For example, we can declare types to represent false equalities:

λ> 2 + 2 = 5
4 = 5 : Type
λ> 2 = "wombat"
2 = "wombat" : Type

However, the only constructor for the = is Refl, and we can only use it when the two arguments are equal.

λΠ> the (4 = 4) Refl
Refl : 4 = 4
λΠ> the (4 = 5) Refl
... type mismatch

So now I'm trying to understand cong by experimenting with it in the REPL. The function cong proves that if two values are equal, applying a function to them produces an equal result. I found the definition.

  cong : {f : t -> u} -> (a = b) -> f a = f b
  cong Refl = Refl

So, for example, if I define...

λ> :let twoEqTwo = the (2 = 2) Refl
defined

...then I expected to be able to show that adding 1 to both sides results in another equality.

λΠ> :let ty = (S 2 = S 2)
defined
λΠ> the ty (cong twoEqTwo)
    ...type mismatch

Can anyone show me an example or two of using cong in the REPL?

HTNW HTNW · Accepted Answer · 2019-05-06T00:27:01

The 2s are of the wrong type. They have defaulted to the type Integer in twoEqTwo, because they have no other constraints. See, an unconstrained 2:

idris> 2
2 : Integer

Yet, in ty, you say S 2. The S forces the whole thing to work in Nat:

idris> S 2
3 : Nat

Make twoEqTwo work in Nat, too:

idris> :let twoEqTwo = the (the Nat 2 = 2) Refl
idris> the (S 2 = S 2) twoEqTwo
Refl : 3 = 3

Note that type inference can sort this out itself if you let it see the entire expression:

idris> the (S 2 = S 2) (cong (the (2 = 2) Refl))
Refl : 3 = 3

Experimenting with cong in the Idris REPL

1 Answers