# 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 sameIntegeras`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 (**c**ontents
of the **a**ddress **r**egister and **c**ontents of the **d**ecrement **r**egister) 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.