December 25, 2021

<aside> 👉 This article can be treated as an extended version of "The Little Typer"

</aside>

Nat stands for Natural Number.

In Pie, four eliminators of Nat: which-Nat, iter-Nat, rec-Nat and ind-Nat are introduced for safe (guarded) recursive style. And we know in ordinary typed languages like Coq, pattern matching is chosen as a primitive and only way to eliminate data constructor. To demonstrate two different flavours of eliminating, I am going to desugar these four Nat eliminators in a pattern matching style in Coq, and see how it captures the idea of safe recursion which ensures that function always terminates.

<aside> 💡 Termination Checking: Dependent Types at Work (Chapter 2.7)

</aside>

Let's start with which-Nat, introduced as the first eliminator for Nat. The usage of which-Nat is simply removing its constructor (add1 in Pie, S in Coq) and then applying operation on a smaller one. It's primitive in Pie and can be defined in Coq below:

Definition which_nat {A : Type} (target : nat) (base : A) (step : nat -> A) : A :=
match target with
  | O   => base
  | S n => step n
end.

Believe it or not, it's all we need for implementing any opeartions on Nat if you are familiar with recursion. For example addition of two Nats:

Fixpoint addition (n : nat) (m : nat) : nat :=
  which_nat n m (fun p => S (addition p m)).

We can compare it with the official implementation in Coq.

Nat.add =
fix add (n m : nat) : nat := match n with
                             | 0   => m
                             | S p => S (add p m)
end.

Obviously authors are not satified with single which-Nat because "recursion is not an option" as they repeated. Unrestricted recursion could lead program never terminate. Coq owns positivity check to avoid such situations but that's not appropriate for a minimial language like Pie. Thus they introduce iter-Nat, which captures a guarded recursion pattern.

Fixpoint iter_nat {A : Type} (target : nat) (base : A) (step : A -> A) : A :=
match target with
  | O   => base
  | S n => step (iter_nat n base step)
end.

Thus the addition could be implemented, returning the ability of recursion back to language itself.

Definition addition_iter (n : nat) (m : nat) : nat :=
  iter_nat n m S.

We can go back to check the implementation of Nat.add again: the abstracted part become smaller: only S (add1 in Pie). It can be understood that which-Nat destructs n and then pass the smaller n to the lambda function (3rd argument); iter-Nat destructs n and pass the result of orginal funtion with same set of arguments (but with smaller n) to the lambda function.

Let's give it a try to apply the idea of iter-Nat to the implementation of gauss addition, we shall know: iter-Nat desturcts Nat and pass the result of functional call with smaller Nat to the function.

Definition gauss_iter (n : nat) : nat :=
  iter_nat n 0 (fun r => n + r).

Dumbs like me could've somehow implemented gauss_iter above but it's completely wrong. Check the correct pattern matching implementation:

Fixpoint gauss_pm (n : nat) : nat :=
match n with
  | O    => 0
  | S n1 => S n1 + gauss_pm n1
end.