Why is the normal form of an ind-Nat expression with a function type an elimination-of-a-function expression

Question

In this question, I am talking about the language Pie described in the book The Little Typer.

Consider the definition

(claim foo-or-bar (-> Nat Atom Atom))
(define foo-or-bar
  (λ (n) (ind-Nat n
           (λ (n) (-> Atom Atom))
           (λ (a) 'foo)
           (λ (n-1 result_n-1 a) 'bar))))

If I then type foo-or-bar on a separate line and execute, Pie outputs

(the (→ Nat Atom
       Atom)
  (λ (n x₁)
    ((ind-Nat n
        (λ (n₁)
          (→ Atom
            Atom))
        (λ (a)
          'foo)
        (λ (n-1 result_n-1 a)
          'bar))
      x₁)))

So, Pie says that the second code snippet is the normal form of foo-or-bar. It's pretty clear why

(λ (n x₁)
  ((ind-Nat n
     (λ (n₁)
       (→ Atom
         Atom))
     (λ (a)
       'foo)
     (λ (n-1 result_n-1 a)
       'bar))
    x₁))

is the same (-> Nat Atom Atom) as

(λ (n) (ind-Nat n
           (λ (n) (-> Atom Atom))
           (λ (a) 'foo)
           (λ (n-1 result_n-1 a) 'bar)))

It's by The Final Second Commandment of lambda, which says

If f is a (Pi ((y Y)) X), and y does not occur in f, then f is the same as (lambda (y) (f y)).

But The Little Typer say that the normal form of an expression is the most direct way of writing it. And, frankly, what I wrote in the definition of foo-or-bar seems more direct than what Pie says its normal form is. So, why is that the normal form? I remember the book said somewhere that if f is a neutral expression of a Pi type, then (lambda (x) (f x) is the normal form of f. This seems similar to the situation with foo-or-bar but not directly applicable.

Answer 1

There are 2 questions here.

The first one is whether the situation is applicable. In fact it is! This is because $(\lambda (x\ y)\ f)$ is abbreviation for $(\lambda (x)\ (\lambda (y)\ f))$. So you apply that in the inner layer.

The second question is why $(\lambda (x)\ (f\ x))$ is more "direct" than $f$. This is because $\lambda$ is the only way to create a $\Pi$ type. Thus it would be more direct to explicitly convey this knowledge. Remember that "direct" doesn't mean short or concise. For example, 10000000000 is a much more direct way to write $10^{10}$ but it is much longer.

The Little Typer chose to use a more blurry definition. But in practice it is well-defined. Only when the type is $\mathbb N, A+B, \mathcal U$, should a neutral term of that type be normal.