# The type of ind-Nat in the pie language?
**URL:** https://racket.discourse.group/t/the-type-of-ind-nat-in-the-pie-language/1733
**Category:** Questions & Answers
**Created:** [February 23, 2023, 2:57am UTC](https://racket.discourse.group/t/the-type-of-ind-nat-in-the-pie-language/1733 "2023-02-23T02:57:32Z")
**Posts on this page:** 5
**Page:** 1
### Author:  [@rebcabin](https://racket.discourse.group/u/rebcabin)
#### Post date: [February 23, 2023, 2:57am UTC](https://racket.discourse.group/t/the-type-of-ind-nat-in-the-pie-language/1733/1 "2023-02-23T02:57:32Z")
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](https://docs.racket-lang.org/pie/#%28def._%28%28lib._pie%2Fmain..rkt%29._ind-.Nat%29%29). Which states:
```plaintext
(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:
```plaintext
(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:
```scheme
; 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 `claim`s 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`?
---
### Author:  [@jbclements](https://racket.discourse.group/u/jbclements)
#### Post date: [February 23, 2023, 9:48pm UTC](https://racket.discourse.group/t/the-type-of-ind-nat-in-the-pie-language/1733/2 "2023-02-23T21:48:31Z")
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
```scheme
(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)
```
??
---
### Author:  [@rebcabin](https://racket.discourse.group/u/rebcabin)
#### Post date: [February 23, 2023, 11:05pm UTC](https://racket.discourse.group/t/the-type-of-ind-nat-in-the-pie-language/1733/3 "2023-02-23T23:05:51Z")
Thanks! That was enough of an idea to get me over the line (and I learned something about nested Pi)!
```plaintext
(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)
```
---
### Author:  [@rebcabin](https://racket.discourse.group/u/rebcabin)
#### Post date: [February 24, 2023, 9:06pm UTC](https://racket.discourse.group/t/the-type-of-ind-nat-in-the-pie-language/1733/4 "2023-02-24T21:06:21Z")
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.
---
### Author:  [@david-christiansen](https://racket.discourse.group/u/david-christiansen)
#### Post date: [March 1, 2023, 10:03am UTC](https://racket.discourse.group/t/the-type-of-ind-nat-in-the-pie-language/1733/5 "2023-03-01T10:03:07Z")
`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))`.