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 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
is a String, and
33 is an Integer in other languages, here
an Atom. So the first type of judgement is stating that something is a
_ 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:
33is the same as
is nonsensical, the right thing to say is:
33is the same Integer as
If we think about it
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 are anything with a value (not quite right but sort of), a
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.
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
(cons 'hello 33) is an expression and is a value by
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)
(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
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
(cons 'hello 33).
If you’re not familiar with Lisp, both
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
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:
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
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
zero and a successor function. Defining the
one is done like
(claim one Nat) (define one (add1 zero))
claim that the name
one is a
Nat and is defined as the
zero using the
add1 constructor. These are known as the
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.