Disclaimer: This post was translated into English by an AI model. It may contain mistakes or awkward wording.

This post is about dependent types. Many people, even programmers with years of experience, may not have encountered the idea. In short, if a type depends on something that is not itself a type, it is a dependent type. I am not an expert on this topic, so why did I suddenly decide to write about it? Because I just finished reading The Little Typer, found it fresh and fascinating, and wanted to write something down. If I can share some of that fun with you, I will be very happy. (^_^)

This post is mostly based on the Pie language described in The Little Typer. I assume the reader has a little background:

some familiarity with Lisp;
basic logic, such as or, and, not, and universal quantification.

My understanding is limited, so mistakes are inevitable. Corrections are welcome.

Come In and Refresh Your Worldview

Pie supports dependent types, so it differs greatly from ordinary languages. Ready? Let us start rebuilding our worldview: of types, values, and execution.

What Is an Expression?

First, a silly question: what are the following things?

0
'a
(+ 0 1)
(add1 zero)
Nat
(Pair Atom Atom)

You probably already have some answers in mind. The answer is: right now, they mean nothing. We have not defined anything yet. Because a language with dependent types can be quite different from languages you already know, please read the definitions carefully and do not assume things work as usual.

Fortunately, everyone here knows some Lisp. With that background, the answer becomes: they are all expressions. Expressions have two aspects:

when they are meaningful;
when two different expressions are the same. Note that "same" and "equal" are not the same idea.

In Pie, everything is an expression. Skeptical? Let us continue.

What Is a Type?

A type is an expression that describes other expressions. This sounds too abstract. What does it mean?

For example, the type of 0 is Nat; in other words, 0 is a Nat. The word "type" itself is not that special. It is just a property of an expression.

Does every expression have another expression describing it? No. Pie has a special type U (Universe), which describes every type except itself. That is, the type of Nat is U, and the type of (→ Atom Nat) is also U.

What Is a Value?

A value is an expression whose top is a constructor. To understand this sentence, we first need to explain constructors.

Every inductively defined type has a base case. For example, Pie's Nat is inductively defined:

zero is a Nat;
if x is a Nat, then (add1 x) is also a Nat.

These two rules define all natural numbers. In Pie, 0 is shorthand for zero, 1 is shorthand for (add1 zero), 2 is shorthand for (add1 (add1 zero)), and so on.

Here, zero and add1 are both constructors. Why call them constructors? Because they construct values. This is a little circular, but useful.

Although add1 looks like a function, we do not treat it as a function here. So 1, 2, 3, and so on are values because their top is add1; 0 is a value; and all atoms are values.

What about types? (→ Nat Nat) means a function type whose argument type is Nat and whose return type is Nat. One possible value of this type is (λ (x) (add1 x)). Here both λ and → are constructors: one constructs function values, the other constructs function types.

What Are Evaluation and Sameness?

Evaluation means turning an expression into a value. For example:

(+ 1 (+ 2 3))

can evaluate to:

(add1 (+ 1 1))

I will not give the definition of + here; just read it as addition.

Yes, it has not finished calculating. But it is already a value. Do not forget that a value is still an expression; it merely has a constructor at the top. This is completely different from languages such as C.

Now we face a difficulty. If values themselves can be written in multiple forms, how do we decide whether two expressions are the same? Intuitively, we find the simplest written form and compare whether they look identical. Exactly. This simplest written form is called the normal form.

In general, normalizing an expression repeatedly computes inner expressions and makes the whole expression shorter. But before normalization, we first evaluate. For example, a one-argument function

evaluates to

(λ (x) (f x))

This is already the simplest way to write it; it is the normal form of f. Unexpectedly, normalization made the expression longer.

Program execution is repeated evaluation. In Pie, everything is an expression, so every program run is simply symbolic manipulation.

Pi Types

Π is another constructor. It constructs values of type U (that is, types), and the resulting type may depend on something that is not a type. This is the first thing we encounter that constructs dependent types.

If A is a type and D is a type, then

(Π ((X A)) D)

is also a type. Its values look like:

(λ (x) [body])

If f has type (Π ((X B)) C), and b has type B, then (f b) has type C, with every X consistently replaced by b. For example:

(Π ((E U)
    (n Nat))
  (→ (Vec E n)
      Nat))

(Vec E n) is, as the name suggests, a vector whose element type is E and whose length is n. The type above can describe a function that computes the length of a vector. Notice that n itself is not a type, so this is more powerful than generics in some languages, which can only range over types.

Sigma Types

Σ is another type constructor that can build dependent types.

Values of (Σ ((x A)) D) have the shape (cons [x] [y]), where both A and D must be type expressions. Here [x] has type A, and [y] has type D, with every x replaced by (car [x]). Put simply, the type of cdr depends on car.

For example:

(Π ((E U))
  (Σ ((k Nat))
    (Vec E k)))

One possible value is (cons 3 (replicate Atom 3 'a)). A function with this type might produce a vector of random length and random content. If k were written in the Π expression instead, the length would be fixed by the argument, which is not what we want.

The difference between Σ and Π is this: for Π, the final expression's type is determined by the expression passed in; for Σ, the final expression's type is determined by the expression passed out, namely the car.

What Are Dependent Types Good For?

What is the point of all this? The meaning comes from the Curry-Howard correspondence: types are propositions, and programs are proofs.

Introduce a new type constructor =, whose type is:

(Σ ((X U))
  (→ X X
    U)))

This means (= Nat 0 0) is a proposition, namely 0 = 0. How do we prove it? By giving an expression of that type:

(claim zero=zero
  (= Nat 0 0))
(define zero=zero
  (same Nat 0))

Here (same E x) produces a value of type (= E x x), where E is a type and x has type E.

Dependent types can therefore place values inside types, thereby constructing propositions about values. This lets us use type-level computation to check properties of programs.

It is then easy to see:

→ corresponds to implication. If a function f has type (→ A B), and a has type A (that is, a proof of A), then (f a) is a proof of B.
Π corresponds to universal quantification, because the function must produce a corresponding proof for every argument.
Σ corresponds to existential quantification, because car and cdr together form a constructive proof.

Through this correspondence, we can express logical propositions as types and ask Pie to compute and check them. Many dependent-type languages end up as theorem provers because they really are that powerful.

One more question: how do we express the proposition ¬A? If ¬A is true, then A cannot hold, meaning A has no proof; it describes no expression. We introduce a basic type Absurd, which describes no expression. By the principle of explosion, if A has a proof, then Absurd also has a proof, so (→ A Absurd) is true. Thus we directly define ¬A as (→ A Absurd).

Review

This post covered:

expressions, types, values, evaluation, and normal forms, all of which differ greatly from mainstream languages;
what dependent types are and how to construct them;
how to represent propositions as types, and what dependent types are useful for.

Since I only wrote about ideas that I personally found interesting and skipped almost everything else, this is quite brief. Please dig into the details on your own.

Appendix

`Atom`, `Nat`, `→`, `Pair`

Atom (Atom): a single quote followed by letters is an atom, such as 'a or 'madoka.
Natural numbers (Nat): zero is a natural number. If x is a natural number, (add1 x) is also a natural number.
Pair (Pair): (cons x y).
Function (→): (lambda (...) ...).