ind-Nat not strictly more powerful than iter-Nat?

[racko]

While re-implementing Pie I avoided unnecessary eliminators and added them as Pie definitions instead. Because of that I tried to implement Fin using ind-Nat, but failed, because "U is a type, but it does not have a type."

(claim Maybe (-> U U))
(define Maybe (lambda (X) (Either X Trivial)))

(claim Fin (-> Nat U))
;(define Fin (lambda (n) (iter-Nat n Absurd Maybe)))
(define Fin (lambda (n) (ind-Nat
                          n
                          (lambda (k) U)
                          Absurd
                          (lambda (smaller acc) (Maybe acc)))))

As far as I understand, Fin cannot be implemented with ind-Nat because of this. Is this intentional? Am I missing something?

PS:
Of course I couldn't implement it with my version of iter-Nat either, because I had to provide a type again:

(claim iter-Nat2 (Pi ((X U)) (-> Nat X (-> X X) X)))
(define iter-Nat2 (lambda (X target base step)
                    (ind-Nat
                      target
                      (lambda (n) X)
                      base
                      (lambda (smaller acc) (step acc)))))
(define Fin (lambda (n) (iter-Nat2 U n Absurd Maybe)))

[david-christiansen]

You're right.

From the perspective of computation alone, ind-Nat is the most general eliminator. It computes identically to rec-Nat. However, due to a design decision that we made to simplify Pie, it's not possible to give a type to every function using ind-Nat.

If elaboration is ignored, then the typing rule for ind-Nat is something like this:

 Γ ⊢ tgt ⇐ Nat
 Γ ⊢ mot ⇐ (→ Nat U)
 Γ ⊢ base ⇐ (mot zero)
 Γ ⊢ step ⇐ (Π ((n Nat)) (→ (mot n) (mot (add1 n))))
----------------------------------------------------
 Γ ⊢ (ind-Nat tgt mot base step) ⇒ (mot tgt)

Note that the motive has to be something that can be checked against a type. This means that it can't be U itself.

There's two ways to design around this limitation:

1. More universes than just U
2. Use a different judgment to assign a type to the motive

For option 1, we could replace the universe rules with something like:

----------------
 Γ ⊢ (U n) type

 n < k
-------------------
 Γ ⊢ (U n) ⇐ (U k)

(where n is a natural number indicating the universe level)

This opens the door to lots of design decisions after that, such as whether to have a kind of "universe level Pi type" or to have cumulativity, where if A : (U n) then A : (U n+1). All of these make type checking a lot more complicated. We used to have it in Pie, but we took it out because we didn't need it for the book and wanted to keep things as simple as possible.

The other good option would be to replace the grammar of ind-Nat with something like:
(ind-Nat tgt ((x) mot) base step)
and then use this rule:

 Γ ⊢ tgt ⇐ Nat
 Γ, x : Nat ⊢ mot type
 Γ ⊢ base ⇐ (mot zero)
 Γ ⊢ step ⇐ (Π ((n Nat)) (→ [n/x]mot [(add1 n)/x]mot))
----------------------------------------------------
 Γ ⊢ (ind-Nat tgt mot base step) ⇒ [tgt/x]mot

In other words, instead of relying on lambda and functions for the motive, use a direct judgment of typehood and a primitive binding form. This is much simpler to implement than all those universes, but it does make it more complicated to explain how induction works.

We went with a simple choice that has some limitations. You're encountering those limitations now!

Because this isn't a bug in this implementation of Pie, I'm going to close this issue. Please feel free to get in touch with further questions!