Reading Notes: The Little Typer — first half

The great book is written by Prof. Daniel P. Friedman and
David Thrane Christiansen, the website is The Little Typer. It introduces dependent type using a small language, Pie.

I am perusing this book since the Spring Festival and writing the thoughts and my understand here.

Types and Expressions

Pie is a language to teach dependent type. So at the very beginning, we have to understand some key concepts and feel the tastes of this book. Thy syntax is lisp-style and many concepts are very similar to Scheme.

Some key points are:

Types are also expressions in Pie, and they are the expressions that describing other expressions. (Q: Can type describe type?)
Everything in Pie is expression. Values in pie is also expressions.
Evaluation in Pie is:
- given a type X of the original expression A
- find another expression B that B is a value
- B is also described by type X
- The progress of finding B is called evaluation
To determine two expressions (values)’s sameness, we have to first have a type
Pie is not Turing-complete, because every function (lambda expression) has to be complete (always has a value). And it does not support recursive syntax. In coq, you can use fixpoint keyword to take advantage of recursive syntax, but coq also only supports complete function (it only accepts those recursive calls with “decreasing” parameter).
Recursive algorithms in Pie are working on Inductive structures (List, Nat, Vector…), these algorithms are implemented via some helper functions (the note will take about them later) which-Nat, rec-Nat, … They have good abstraction of the working logic, the kind of skills seem like continuation (encoding what to do next in a function).

Nats

Nat is an induction type that describe natural numbers.

Nat :: zero
     | add1 Nat

There are some important expressions that can help us to understand the basic knowledge of type in Pie (this is the cornerstone of understanding dependent types).

NB: it is important to focus on the type behavior before trying to write code using the following expressions.

which-Nat

(which-Nat target base step)
;; semantic is shown below demo-code
case target of
     0    -> base
   add1 m -> step m
end

In the above expression:

target is the recursive (inductive) structure we want to work on, its type has to be Nat.
base is one potential result. It is the result when we do not need to unpack the target. It can be any type and it has to have a type.
step is a lambda expression, it is the key to unpack the inductive structure (Nat), its type is (-> Nat X) (given that base is a X).
the whole which-Nat expression is a X

Let’s write a function to make sure we understand the above knowledge. How about writing a function to check if a Nat is larger than 0?

(claim larger-than-zero
  (-> Nat Atom))

(define larger-than-zero
  (lambda (n)
    (which-Nat n
      'f
      (lambda (m)
        't))))

One thing on which-Nat I want to say is that: it does not contain memory, all the information is passed, we just continue going. This is because the step function only contains one parameter of the inductive structure (no parameter of history status). The rest of Nat related expressions can have history as parameter so that their ability is more powerful than which-Nat. Anyway this is good for starting.

rec-Nat

This expression has more power than the first one because the it can remember some of the history.

(rec-Nat target base step)
;; semantic is shown in below demo-code
case target of
    0    -> base
  add1 m -> step m (rec-Nat m base step)

The type rules of it is:

target is the inductive structure that we want to work on, its type is Nat
base is one potential result. It is the result when we do not need to unpack the target. It can be any type and it has to have a type.
step is a lambda expression, it is the key to unpack the inductive structure (Nat), its type is (-> Nat X X), the X here is the X of the type of base

step can be seen as continuation.

Let’s use this function to write an example to compute the sum $f(n) = \sum_{i=0}^{n}i$ .

(claim plus
  (-> Nat Nat Nat))

(define plus
  (lambda (a b)
    (rec-Nat a
      b
      (lambda (m r)
        (add1 r)))))

(claim sum
  (-> Nat Nat))

(define sum
  (lambda (n)
    (rec-Nat n
      0
      (lambda (m r)
        (plus (add1 m) r)))))

It seems hard to write a function to compute the nth Fibonacci number using only rec-Nat. Is it possible?

iter-Nat

This one is nothing new. Let me skip it and continue.

Generic Programming and List

Then we come to list and vector types. They can give us the idea of generic programming (IIUC).

This need PI expression to claim the types of some generic functions. Some examples are good to make sure we understand.

It should be noted that: for all the expressions that helping us do recursive, rec-Nat, ref-list, their parameter base should be first deduced a type, otherwise, the expression does not type check. When you want to use nil, you have to use the expression to provide the type information.

Let me write some generic list functions to check the knowledge.

#lang pie
(claim myappend
  (Pi ((E U))
    (-> (List E) (List E) (List E))))

(define myappend
  (lambda (E)
    (lambda (l1 l2)
      (rec-List l1
        l2
        (lambda (hd tl l)
          (:: hd l))))))

(claim myreverse
  (Pi ((E U))
    (-> (List E) (List E))))

(define myreverse
  (lambda (E)
    (lambda (l)
      (rec-List l
        (the (List E) nil)
        (lambda (hd tl r)
          ((myappend E) r (:: hd nil)))))))

(claim myduplicate
  (Pi ((E U))
    (-> E Nat (List E))))

(define myduplicate
  (lambda (E)
    (lambda (elem n)
      (rec-Nat n
        (the (List E) nil)
        (lambda (m r)
          (:: elem r))))))

Vector: the first glance at dependent type

All the previous sections talks about nothing new. You can find all the above content in common functional programming languages like ML, Coq. We can construct new types using types. But now, we come to a new world: we can construct types using something that is not a type. This is dependent type.

Let’s first look at C’s array as an example:

int a[10];
int b[20];
void loop_array(int a[], int len);
/* loop_array(a, 10) is type check */
/* loop_array(b, 20) is also type check */

The type of a and b above are the same, they are both int [].

This is not good since array out-of-bound bug is hard to debug and sometimes they do not error out that making things worse.

Typing laws of vector

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), then (vec:: e es) is a (Vec E (add1 k)).

Laws of Pi

The expression (Pi ((y Y)) X) is a type when Y is a type, and X is a type when y is a Y.

Laws of lambda

If x is an X when y is a Y, then (lambda (y) x) is a (Pi ((y Y)) X).

Dependent types

First paste the definition of dependent type here:

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

Vector is a very good example. We can know if there is out-of-bound error at compiling time.

Why rec-Nat is not enough?

Can we use all our old friends (rec-Nat, iter-Nat, …) to implement a function that duplicates elements and returns a vector? To make thing simpler, write a function that take a Nat as input and produce a vector whose length is just the input Nat and all the elements in it is the number 1 (something like (duplicate-vec 5) => [1 1 1 1 1]): .

rec-Nat cannot finish the job because, the base in rec-Nat has to be the same type as the parameter passing to step. This is impossible because base is vecnil,a (Vec Nat 0).

So to deal with recurrent involving dependent types, we have to come to one new friend: int-Nat.

(claim mot-dup
  (-> Nat U))

(define mot-dup
  (lambda (n)
    (Vec Nat n)))

(claim dup-vec
  (Pi ((n Nat))
    (Vec Nat n)))

(define dup-vec
  (lambda (n)
    (ind-Nat n mot-dup
      (the (Vec Nat 0) vecnil)
      (lambda (m r)
        (vec:: zero r)))))

We introduce an extra parameter mot-dup to make the program type checking. It is a function that taking into the target to compute the type, and based on the computed type we type check each part of the ind-Nat expression.

Now let’s go one step further, can we write a function that can duplicate any type of elements? Like ((dup-vec Atom) 3 'a) -> ['a 'a 'a]

(claim mot-dup-vec
  (Pi ((E U))
    (-> Nat U)))

(define mot-dup-vec
  (lambda (E)
    (lambda (n)
      (Vec E n))))

(claim dup-vec
  (Pi ((E U)
       (n Nat))
    (-> E (Vec E n))))

(define dup-vec
  (lambda (E)
    (lambda (n)
      (lambda (elem)
        (ind-Nat
          n
          (mot-dup-vec E)
          (the (Vec E 0) vecnil)
          (lambda (m r)
            (vec:: elem r)))))))

Key to understand ind-nat is that we introduce motive because simply comparing two types are not enough that we have to use some functions to transform the types before comparing them.

Some programs

Compute max

#lang pie

(claim minus
  (-> Nat Nat Nat))

;; 3 - 4 = 0
;; 4 - 2 = 2
(define minus
  (lambda (a b)
    (rec-Nat
      b
      a
      (lambda (n r)
        (which-Nat
          r
          0
          (lambda (k) k))))))


(claim gt
  (-> Nat Nat Nat))
;; 4 >= 3 --> 1
;; 3 >= 4 --> 0
(define gt
  (lambda (a b)
    (which-Nat
      (minus a b)
      0
      (lambda (x) 1))))

(claim max
  (-> Nat Nat Nat))

(define max
  (lambda (a b)
    (which-Nat
      (gt a b)
      b
      (lambda (k) a))))

End of First Half

After finishing the first half of the book, now let me share some feelings (feeling from guy who first touch dependent type):

Dependent types introduce mechanisms to make program safe. This adds overhead for programmer when writing code (but no overhead in runtime). Types become one thing programmers need to code.

Thoughts on Computing

英雄无岁，江湖无辈