Using replace in Idris
This is a fairly technical post on Idris: a dependently-typed functional language. It will likely be of interest only to other Idris learners. I'm working on a longer post on dependent types, Idris, and proof that will (hopefully) be of more general interest.
The use of replace & rewrite in Idris has been the subject of some confusion. I think I've gotten comfortable with replace, at least, and I wanted write it down. Like Martin John Baker (in the first link) "for some reason I don't feel I am going to understand rewrite fully unless I can do it using replace."
If, in the Idris REPL, we say :doc replace, we are told:
Builtin.replace : {0 p : _ -> Type} -> (0 _ : x = y) -> (1 _ : p x) -> p y
Perform substitution in a term according to some equality.
Totality: total
Visibility: public export
So: given a predicate \(p\) on some (un-named) type, and given a proof term for the claim that \(x\) is propositionally equal to \(y\), and given an element of type \(p \enspace x\), then we get an element in \(p \enspace y\). I get the premise: if \(x = y\), then for all predicates \(p\) we have \(p \enspace x = p \enspace y\). What confused me was how to actually make use of this.
Let's take a simple example from Functional Programming in Idris 2: we wish to write the following function:
replaceVect : Vect (n + 0) a -> Vect n a
You see the problem: to the type checker, Vect (n + 0) a and Vect n a are different types. We proceed, using replace:
replaceVect : Vect (n + 0) a -> Vect n a replaceVect xs = replace {p = {- pred -}} {- proof: x = y -} xs
Nb that this won't type-check; I couldn't even setup holes for this. It's just a skeleton of my intended implementation using comments. The problem as I see it is that the problem is under-determined: we need to pick \(x\), \(y\) and \(p\) such that:
- \(p \enspace x = Vect \enspace (n + 0) \enspace a\)
- \(p \enspace y = Vect \enspace n \enspace a\)
and such that we can prove to the type-checker that \(x = y\).
If we notice that picking \(p\) to be \(k \rightarrow Vect \enspace k \enspace a\), then \(x\) & \(y\) fall right out: \(x = n + 0\) and \(y = n\). This leaves us with:
replaceVect : Vect (n + 0) a -> Vect n a replaceVect xs = replace {p = \k => Vect k a} {- proof: n + 0 = n -} xs
Now we need, for any \(n\), a proof that \(n + 0 = n\). OK, well, that would look like a function from \(n:\mathbb{N}\) into the proposition \(n + 0 = n\):
addZeroRight : (n : Nat) -> n + 0 = n
A little clause adding, case splitting and proof search gives us:
addZeroRight : (n : Nat) -> n + 0 = n addZeroRight 0 = Refl addZeroRight (S k) = ?addZeroRight_rhs_1
Thinking from the logic side of this, we're writing a proof by induction: we've got the base case (i.e. zero) and now we need the inductive case. Except we're on the computational side, writing a function. The computational analogue of induction is recursion: what if we called ourselves on \(k\)?
addZeroRight : (n : Nat) -> n + 0 = n addZeroRight 0 = Refl addZeroRight (S k) = ?addZeroRight_rhs_1 (addZeroRight k)
Idris now tells us what we have & what we need to complete the function:
k : Nat ------------------------------ addZeroRight_rhs_1 : plus k 0 = k -> S (plus k 0) = S k
This is a job for cong. If, again in the REPL, we say :doc cong, Idris tells us
Prelude.cong : (0 f : (t -> u)) -> (0 _ : a = b) -> f a = f b Equality is a congruence. Totality: total Visibility: public export
So: if we have a proof that \(k + 0 = k\) (which we do: that's just \((addZeroRight \enspace k)\)), then \(cong \enspace S\) will give us \(S \enspace (k + 0) = S \enspace k\)– just what we need:
addZeroRight : (n : Nat) -> n + 0 = n addZeroRight 0 = Refl addZeroRight (S k) = cong S (addZeroRight k)
That's it! Now, for any \(n\), \(addToZeroRight \enspace n\) produces a proof term for the proposition \(n + 0 = n\); just what we needed to make replace work:
replaceVect : Vect (n + 0) a -> Vect n a replaceVect xs = replace {p = \k => Vect k a} (addZeroRight n) xs
So, for now, my mental model of replace is this: compare the type you have to the type you want. They're likely structurally very similar. Construct a predicate \(p\) that expresses that structure– the argument to \(p\) should pick-out the difference between the type you have & the type you want. \(x\) & \(y\) will be the corresponding arguments to \(p\). Then, if you can find yourself a proof that \(x = y\), you're good to go.
10/14/24 18:36