What is an explanation of the replace operator in the Pie language?

Question

This is the first concept in The Little Typer to give me quite a bit of trouble, and it appears I am not alone (1 2), so perhaps it would be beneficial to ask here. Hopefully this can be connected with more general concepts to expand the audience for this question beyond people reading the book.

The textbook The Little Typer is an introduction to dependent types using the Pie language. Chapter 8 introduces the concept of expressing statements with types, and constructing a value of that type being a proof of that statement being true.

In Pie, the type statement that two expressions are equal is (= X from to) [docs], where = is the type constructor, X is a type, and both from and to are values of type X. For example (= Nat (+ 6 6) (+ 8 4)).

The value constructor of = is same, where (same e) has type (= X e e) if e is an X. So the value (same 12) is a proof & instance of type (= Nat (+ 6 6) (+ 8 4)) (that doesn't require induction to construct).

The = type also has an eliminator called cong (short for congruent) where (cong target f) transforms a target of type (= X from to) to type (= Y (f from) (f to)), where f is of type (→ X Y). For example (λ(n) (cong (same n) (+ 1))) evaluates to (λ(n) same (+ 1 n).

Here's where I have trouble: chapter 9 introduces a more general eliminator for = called replace and claims replace can do anything cong can do, and more. The definition of replace is:

(replace target motive base) → (motive to)
  target : (= X from to)
  motive : (→ X U)
  base : (motive from)

Frankly I can't make heads nor tails of this operator. How would I parameterize it to mimic cong? What is an example of something it can do that cong cannot? The only clue I have to its workings is its name and the context in which it's presented, where I assume what we're doing is transforming one expression to look like something else.

Answer 1

I'll rewrite cong in terms of replace. This should also explain how replace works along the way.

We have (= X a b) and want to produce (= Y f(a) f(b)). But notice that we already have (= Y f(a) f(a)) from (same f(a)). So ideally we want to replace the second a in (= Y f(a) f(a)) with a b. replace allows us do exactly that.

Here target is what we want to use to replace. We choose:

target is (= X a b), from is a, to is b

Now base is the expression in which we want to replace something.

base as (= Y f(a) f(a))

How should we choose motive such that motive to is (= Y f(a) f(b)) and motive from is (= Y f(a) f(a))?

motive x ->  (= Y f(a) f(x))

works! Thus we have implemented cong as:

cong target f -> replace target (lambda x -> (= Y f(a) f(x))) (same f(a))
target : (= X a b)
f : (-> X Y)

Sorry for the abuse of notation, I'm familiar with type theory but not Pie specifically. So all in all we have (= Y f(a) f(a)) and used (= X a b) to replace one of the as with a b.

Another simpler version of replace (if that helps):

simple_replace target from -> to
target : (= X from to)
from: X