The type of ind-Nat in the pie language?

Questions & Answers
1

Hello -- I am trying to write a type for my own copy of ind-Nat in pie, following the example from the original pie documentation. Which states:

(ind-Nat target motive base step) → (motive target)
target : Nat
motive : (-> Nat U)
base   : (motive zero)
step	 	:	(Π ((n Nat))
           (-> (motive n)
           (motive (add1 n))))

This does not survive a copy-paste into racket's interpreter for reasons I shall not go into.

My best attempt to "make it real," so far, has been:

(claim iN (Π ((E U))
             (→ Nat               ; target
                (→ Nat U)         ; mot, m
                E                 ; base, (m 0)
                (→ Nat E E)       ; step
                E)))              ; result, (m ℓ)

(define iN
  (λ (E)
    (λ (t m b s)
      (ind-Nat
       t
       m
       b
       s))))

which produces an error:

; Expected
;   (m 0)
; but given E 
;   Source locations: (the line with b, the base, on it)

I have tried many permutations of substituting calls of m, with defining claims for b, and so on, all leading nowhere better. I'd like to note that the book, "The Little Typer," which has nice descriptions of all this, does not exhibit a type for ind-Nat, leading me to suspect:

Is this one of those types that is "expressible but not denotable" in the type-system of pie? Should I give up trying to divinate a type for (my copy of) ind-Nat?

1 Like
2

I'm not reading this incredibly carefully, but I ... don't think you're doing it right. In particular, it doesn't make sense to me that (m 0) doesn't show up as the type of your base, and it doesn't look to me like you're using the target as part of a dependent type. Wouldn't the type be more like

(claim iN (Π ((E U) (target Nat) (m (→ Nat ?)))
             (→ (m 0)                 ; base, (m 0)
                (Π ((n Nat)) (→ (m n) (m (add1 n))))       ; step
                (m (add1 n)))))              ; result, (m l)

??

1 Like
3

Thanks! That was enough of an idea to get me over the line (and I learned something about nested Pi)!

(claim iN
       (Π ((t   Nat)
           (m   (→ Nat U))
           (b   (m 0))
           (s   (Π ((n-1 Nat))
                   (→ (m n-1)
                      (m (add1 n-1))))))
          (m t)))

(define iN
  (λ (t m b s)
    (ind-Nat
     t
     m
     b
     s)))


(claim peas-ex
       (Π ((ℓ Nat))
          (Vec Atom ℓ)))

(define peas-ex
  (λ (ℓ)
    (iN ℓ
        mot-peas
        base-peas
        step-peas)))

(peas-ex 0)
(peas-ex 1)
(peas-ex 2)
4

One little observation here is that capital Pi is at least like let* in scheme: later bindings may depend on earlier ones. For instance, b depends on m. I didn't yet try to find out whether it''s like letrec, i.e., that any binding may depend on any other.

5

Pi is like let* in that (Pi ((x A) (y B)) C) is completely equivalent to (Pi ((x A)) (Pi ((y B)) C)). This matches lambda, where (lambda (x y) e) is completely equivalent to (lambda (x) (lambda (y) e)).

2 Likes