Notes on introduction to Dependent Types #1

One of the reasons of existence of this website (my blog site) is for me to “record” whatever thing I’m learning or exploring at the moment, I know now that for me is much harder to do, I don’t have my creative ability as tuned as my “content consuming” ability, but at least I’m going to try. In this occasion I’ll try to document what I can get about Type Level Programming an area that is starting to become of great interest for me but that my head is having trouble keeping up with it.

What ever I’ll write in this post is about the ideas I can grasp about the book “The Little Typer” by Daniel P. Friedman and David Thrane Christiansen, I recommend watching the talk A Little Taste of Dependent Types by one of the authors if you don’t want to read the whole book to see what’s about, or otherwise read this post. Lets begin!

The subject of the book is Type Theory and more specifically Dependent Types, as I understand is a bridge connecting mathematics and programming, the idea is that you can use the Type System of a language that checks your program at compile-time for correctness and in essence it let’s you mathematically prove aspects of your program. So in a way proves are programs that can be run (at compile-time). In the book a custom language called Pie is used, is a Lisp flavoured language, I believe it was based of from Scheme, I will use it too to keep ideas clear but any programming language with a decent type system will do (Scala, Idris, Haskell + GADTs + DataKinds + TypeFamilies).

Judgements

Judgements are things that can be said about expression, is how we express a belief with the knowledge we have up to that point. There are mainly four types of judgements:

1. Type of an expression

In Pie language, an expression that begins with tick mark ' and is followed by letters or hyphens - is an Atom. The same way that "hello" is a String, and 33 is an Integer in other languages, here 'hello is an Atom. So the first type of judgement is stating that something is a something.

_ is a _

2. Sameness with respect to a Type

Saying that something is the same thing as another it only makes sense when said with respect to a Type. Saying that:

33 is the same as 11*3

is nonsensical, the right thing to say is:

33 is the same Integer as 11*3

If we think about it 33 and 11*3 are things that already exists in a universe, to state that they’re indeed the same we must specify in which universe? that is the Integer universe. The book uses Nat (from Natural numbers) and I’m going to switch to that.

_ is the same _ as _

3. Name of a Type

In Pie any expression that begins with a capital letter is a Type. Nat is a type as well as Atom. Saying that something is a type is the third form of judgment.

_ is a type

Note: I have learned that even types have types which are called kinds so a way to see this judgement is as a lifted version of the first judgement, where we say that anything that begins with a capital letter has the kind type? 🤔

4. Sameness of Types

The final form of judgment is saying that two given types are the same, this is a lifted version of the second form of judgement (sameness with respect to a Type), one could say that Atom and Atom are the same type.

_ and _ are the same type

I wonder if sameness of values are with respect to a type, then sameness of types are with respect to a kind? 🤔

Expressions

Expressions are anything with a value (not quite right but sort of), a literal like 33 is an expression (and has a value), an identifier (variable name) and operators are also expressions, the composition of these also form other expressions, so everything is an expression? in Pie it is.

Values

A value is an expression that has a constructor (a value constructor) at the top. In Pie a pair (also known as tuple) is constructed with the construct cons, so (cons 'hello 33) is an expression and is a value by itself.

Types

A type is an expression that has a type constructor at the top and as we said earlier they begin with a capital letter. In Pie a pair (cons 'hello 33) is a (Pair Atom Nat), if Pair expects two other types to yield a type, then it is a type constructor. Atom is in itself the type constructor that accepts no other types as arguments, and yields the type Atom.

Normal form

Every expression (either a value expression or a type expression) has what is called the normal form, this refers to the simplest way of writing such expression. In the same vein of “sameness” asking the normal form of a value expression is always with respect to a Type. It is said that two expressions are the same when they both have identical normal forms, and both expressions having identical normal forms means that those two expressions are the same.

For example, the expression:

(cons
  (car (cons 'hello 'world))
  33)

Is the same (Pair Atom Nat) that the expression:

(cons 'hello 33)

However the latter is in normal form whereas the former is not, that is because the most direct way of writing a (Pair Atom Nat) expression is indeed (cons 'hello 33).

If you’re not familiar with Lisp, both car and cdr are functions that in Pie are called “eliminators”, their names are somewhat arcane (contents of the address register and contents of the decrement register) but all they do is retrieve the first (car) and second (cdr) component of a Pair.

An example of a type expression that is not in the normal form is:

(car
  (cons Atom 33))

This expression expressed in the normal form is:

Atom

Definitions

Lastly, in Pie we can define names with the construct define however we must first use claim to state the type of the name to be defined. Above we used the Nat 33, but it turns out that in Pie is not defined, the only Nat predefined is 0 (also expressed as zero), other numbers are built from zero and a successor function. Defining the Nat one is done like so:

(claim one Nat)
(define one
  (add1 zero))

We first claim that the name one is a Nat and is defined as the successor of zero using the add1 constructor. These are known as the Peano numbers.

Conclusion

These notes are the important concepts to grasp from the first chapter of the book “The Little Typer” by Daniel P. Friedman and David Thrane Christiansen, you can buy your copy here.