3 NOTE: The Little Typer

3.1 Judgement

The four forms of Judgement.

U is Universe, Nat is natural

3.2 eliminator

which-Nat is an eliminator of Nat, it takes three parameters: target, base and step, here are examples:

(add1 n) will be target

3.3 recursive is not an option

To define a + for Nat, we might first write down the following definition, unfortunately, we would get an error: Unknown variable +

(claim + (-> Nat Nat Nat))

(define +

(lambda (n j)

(which-Nat n

j

(lambda (n-1) (add1 (+ n-1 j))))))

Because in Pie, recursive was not an option, the pre-condition was we must have value for each expression, so if there was a recursion, we could get:

(claim forever (-> Nat Atom))

(define forever

(lambda (and-ever)

(forever and-ever)))

To avoid it, recursive is not an option.

3.4 total function

A function assigns a value to every possible argument is called a total function. In Pie, all functions are total.

Total function is important that we always want to get a value from application.

3.5 why is rec-Nat always safe to use

The reason is because rec-Nat guaranteed to reach the base. Every Nat is zero or (add1 n), where n is a smaller Nat.

3.6 elim-Pair to Π

(elim-Pair

A D

X

p

f)

where p is a (Pair A D), and f takes values of the expression from car and cdr from p.

Candidate type of elim-Pair

(-> A D

X

(Pair A D)

(-> A D

X)

X)

But this cannot be true. So we need Π.

Example of Π

(claim flip

(Π ((A U) (D U))

(-> (Pair A D)

(Pair D A))))

(define flip

(lambda (A D)

(lambda (p)

(cons (cdr p) (car p)))))

So basically Π says there has A is U and D is U, and the body of Π following this truth. This also means lambda-expression’s type can be a U-expression.

In the expression

(Π ((A U) (D U)

(-> (Pair A D)

(Pair D A))))

the body of it was:

(-> (Pair A D)

(Pair D A))

Now, we know how to claim type of elim-Pair:

(claim elim-Pair

(Π ((A U)

(D U)

(X U))

(-> (Pair A D)

(-> A D

X)

X)))

(define elim-Pair

(lambda (A D X)

(lambda (p f) (f (car p) (cdr p)))))

3.7 more Π

Type can dependent on Term, Vec is an example:

• If E is a type and k is a Nat, then (Vec E k) is a type.

• vecnil is a (Vec E zero)

• If e is an E and es is a (Vec E k), (vec:: e es) is a (Vec E (add1 k))

To get first element from List in Pie is impossible. Because we cannot sure that’s safe, nil has no entry! But get first element from (Vec E (add1 k)) is possible for every k is Nat.

To define such function, it’s easy to guess Π also takes Term as parameter.

Here we go(with eliminator head and tail):

(claim first

(Π ((E U)

(l Nat))

(-> (Vec E (add1 l))

E)))

(define first

(lambda (E l)

(lambda (es)

(head es))))

and ->-expressions is a shorter way of writing Π-expressions when argument name is not used in the Π-expression’s body. Therefore, the following definition is the same as above:

(claim first

(Π ((E U)

(l Nat))

(Π ((es (Vec E (add1 l))))

E)))

3.8 dependent type

A type is determined by something that is not a type called dependent type.

Now considering a term ‘peas‘ produces many pea. We can though out type quickly:

(claim peas

(Π ((how-many-peas Nat))

(Vec Atom how-many-peas)))

Then we use rec-Nat to implement it:

(define peas

(lambda (how-many-peas)

(rec-Nat how-many-peas

vecnil

(lambda (l-1 peas-l-1)

(vec:: 'pea peas-l-1)))))

Unfortunately, we would get Can’t determine a type as error message.

The problem here is to use rec-Nat, base must has the same type as peas-l-1 argument to the step. But here we get (Vec Atom how-many-peas) and (Vec Atom 0). Therefore, we need something else to complete this job.

3.9 ind-Nat, induction on Nat

To create peas, we need ind-Nat. ind-Nat just like rec-Nat, but allows the types of the base and the almost-answer in the step. ind-Nat is used for dependent types. And (Vec Atom how-many-peas) is a dependent type, when how-many-peas is not a Type!

(claim motive-peas

(-> Nat

U))

(define motive-peas

(lambda (k)

(Vec Atom k)))

The base type of peas is surely (Vec Atom 0). The base value of peas is surely vecnil, because it’s only value has type (Vec Atom 0). (Vec Atom 0) is the same type as (motive-peas 0).

The step type:

(Π ((n-1 Nat))

(-> (motive n-1)

(motive (add1 n-1))))

The almost-answer’s type is motive applied to n-1.

Step for peas:

(claim step-peas

(Π ((l-1 Nat))

(-> (motive-peas l-1)

(motive-peas (add1 l-1)))))

(define step-peas

(lambda (l-1)

(lambda (peas-l-1)

(vec:: 'pea peas-l-1))))

Finally, the definition of peas:

(claim peas

(Π ((how-many-peas Nat))

(Vec Atom how-many-peas)))

(define peas

(lambda (how-many-peas)

(ind-Nat how-many-peas

motive-peas

vecnil

step-peas)))

Building a value of any natural number by giving a value for zero and a way to transform a value for n into a value n+1 called induction on natural numbers.

And we can define a rec-Nat based on ind-Nat:

(claim rec-Nat-2

(Π ((X U))

(-> Nat

X

(-> Nat X

X)

X)))

(define rec-Nat-2

(lambda (X)

(lambda (target base step)

(ind-Nat target

(lambda (k) X)

base

step))))

3.10 type is statement

The expressions ’apple and ’apple are equal Atoms.

For every Nat n, (+ 1 n) equals (add1 n).

if X then Y.

A and D.

there exists.

3.11 Σ type

• A is a type, and

• D is a type if x is an A.