What is a brief but complete explanation of a pure/dependent type system?

Question

If something is simple, then it should be completely explainable with a few words. This can be done for the λ-calculus:

The λ-calculus is a syntactical grammar (basically, a structure) with a reduction rule (which means a search/replace procedure is repeatedly applied to every occurrence of a specific pattern until no such pattern exists).

Grammar:

Term = (Term Term) | (λ Var . Term) | Var

Reduction rule:

((λ var body) term) -> SUBS(body,var,term)
    where `SUBS` replaces all occurrences of `var`
    by `term` in `body`, avoiding name capture.

Examples:

(λ a . a)                             -> (λ a a)
((λ a . (λ b . (b a))) (λ x . x))     -> (λ b . (b (λ x x)))
((λ a . (a a)) (λ x . x))             -> (λ x . x)
((λ a . (λ b . ((b a) a))) (λ x . x)) -> (λ b . ((b (λ x . x)) (λ x . x)))
((λ x . (x x)) (λ x . (x x)))         -> never halts

While somewhat informal, one could argue this is informative enough for a normal human to understand the λ-calculus as a whole - and it takes 22 lines of markdown. I'm trying to understand pure/dependent type systems as used by Idris/Agda and similar projects, but the briefer explanation I could find was Simply Easy - a great paper, but that seems to assume a lot of previous knowledge (Haskell, inductive definitions) that I don't have. I think something briefer, less rich could eliminate some of those barriers. Thus,

Is it possible to give a brief, complete explanation of pure/dependent type systems, in the same format I presented the λ-calculus above?

Answer 1

Disclaimer

This is very informal, as you requested.

The grammar

In a dependently typed language we have a binder at the type level as well as at the value level:

Term = * | (∀ (Var : Term). Term) | (Term Term) | (λ Var. Term) | Var

Well-typed term is a term with attached type, we will write t ∈ σ or

σ
t

to indicate that term t has type σ.

Typing rules

For the sake of simplicity we require that in λ v. t ∈ ∀ (v : σ). τ both λ and ∀ bind the same variable (v in this case).

Rules:

t ∈ σ is well-formed if σ ∈ * and t is in normal form (0)

*            ∈ *                                                 (1)
∀ (v : σ). τ ∈ *             -: σ ∈ *, τ ∈ *                     (2)
λ v. t       ∈ ∀ (v : σ). τ  -: t ∈ τ                            (3)
f x          ∈ SUBS(τ, v, x) -: f ∈ ∀ (v : σ). τ, x ∈ σ          (4)
v            ∈ σ             -: v was introduced by ∀ (v : σ). τ (5)

Thus, * is "the type of all types" (1), ∀ forms types from types (2), lambda abstractions have pi-types (3) and if v is introduced by ∀ (v : σ). τ, then v has type σ (5).

"in normal form" means that we perform as many reductions as possible using the reduction rule:

"The" reduction rule

(λ v. b ∈ ∀ (v : σ). τ) (t ∈ σ) ~> SUBS(b, v, t) ∈ SUBS(τ, v, t)
    where `SUBS` replaces all occurrences of `v`
    by `t` in `τ` and `b`, avoiding name capture.

Or in two-dimensional syntax where

σ
t

means t ∈ σ:

(∀ (v : σ). τ) σ    SUBS(τ, v, t)
                 ~>
(λ  v     . b) t    SUBS(b, v, t)

It's only possible to apply a lambda abstraction to a term when the term has the same type as the variable in the associated forall quantifier. Then we reduce both the lambda abstraction and the forall quantifier in the same way as in the pure lambda calculus before. After subtracting the value level part, we get the (4) typing rule.

An example

Here is the function application operator:

∀ (A : *) (B : A -> *) (f : ∀ (y : A). B y) (x : A). B x
λ  A       B            f                    x     . f x

(we abbreviate ∀ (x : σ). τ to σ -> τ if τ doesn't mention x)

f returns B y for any provided y of type A. We apply f to x, which is of the right type A, and substitute y for x in the ∀ after ., thus f x ∈ SUBS(B y, y, x) ~> f x ∈ B x.

Let's now abbreviate the function application operator as app and apply it to itself:

∀ (A : *) (B : A -> *). ?
λ  A       B          . app ? ? (app A B)

I place ? for terms that we need to provide. First we explicitly introduce and instantiate A and B:

∀ (f : ∀ (y : A). B y) (x : A). B x
app A B

Now we need to unify what we have

∀ (f : ∀ (y : A). B y) (x : A). B x

which is the same as

(∀ (y : A). B y) -> ∀ (x : A). B x

and what app ? ? receives

∀ (x : A'). B' x

This results in

A' ~ ∀ (y : A). B y
B' ~ λ _. ∀ (x : A). B x -- B' ignores its argument

(see also What is predicativity?)

Our expression (after some renaming) becomes

∀ (A : *) (B : A -> *). ?
λ  A       B          . app (∀ (x : A). B x) (λ _. ∀ (x : A). B x) (app A B)

Since for any A, B and f (where f ∈ ∀ (y : A). B y)

∀ (y : A). B y
app A B f

we can instantiate A and B to get (for any f with the appropriate type)

∀ (y : ∀ (x : A). B x). ∀ (x : A). B x
app (∀ (x : A). B x) (λ _. ∀ (x : A). B x) f

and the type signature is equivalent to (∀ (x : A). B x) -> ∀ (x : A). B x.

The whole expression is

∀ (A : *) (B : A -> *). (∀ (x : A). B x) -> ∀ (x : A). B x
λ  A       B          . app (∀ (x : A). B x) (λ _. ∀ (x : A). B x) (app A B)

I.e.

∀ (A : *) (B : A -> *) (f : ∀ (x : A). B x) (x : A). B x
λ  A       B            f                    x     .
    app (∀ (x : A). B x) (λ _. ∀ (x : A). B x) (app A B) f x

which after all reductions at the value level gives the same app back.

So while it requires just a few steps in the pure lambda calculus to get app from app app, in a typed setting (and especially a dependently typed) we also need to care about unification and things become more complex even with some inconsitent convenience (* ∈ *).

Type checking

• If t is * then t ∈ * by (1)
• If t is ∀ (x : σ) τ, σ ∈? *, τ ∈? * (see the note about ∈? below) then t ∈ * by (2)
• If t is f x, f ∈ ∀ (v : σ) τ for some σ and τ, x ∈? σ then t ∈ SUBS(τ, v, x) by (4)
• If t is a variable v, v was introduced by ∀ (v : σ). τ then t ∈ σ by (5)

These all are inference rules, but we can't do the same for lambdas (type inference is undecidable for dependent types). So for lambdas we check (t ∈? σ) rather than infer:

• If t is λ v. b and checked against ∀ (v : σ) τ, b ∈? τ then t ∈ ∀ (v : σ) τ
• If t is something else and checked against σ then infer the type of t using the function above and check whether it is σ

Equality checking for types requires them to be in normal forms, so to decide whether t has type σ we first check that σ has type *. If so, then σ is normalizable (modulo Girard's paradox) and it gets normalized (hence σ becomes well-formed by (0)). SUBS also normalizes expressions to preserve (0).

This is called bidirectional type-checking. With it we don't need to annotate every lambda with a type: if in f x the type of f is known, then x is checked against the type of the argument f receives instead of being inferred and compared for equality (which is also less efficient). But if f is a lambda, it does require an explicit type annotation (annotations are omitted in the grammar and everywhere, you can either add Ann Term Term or λ' (σ : Term) (v : Var) to the constructors).

Also, have a look at the Simpler, Easier! blogpost.

Answer 2

Let's have a go. I'll not bother about Girard's paradox, because it distracts from the central ideas. I will need to introduce some presentational machinery about judgments and derivations and such.

Grammar

Term   ::=   (Elim)   |   *   |   (Var:Term)→Term   |   λVar↦Term

Elim   ::=   Term:Term   |   Var   |   Elim Term

The grammar has two mutually defined forms, "terms" which are the general notion of thing (types are things, values are things), including * (the type of types), dependent function types, and lambda-abstractions, but also embedding "eliminations" (i.e. "usages" rather than "constructions"), which are nested applications where the thing ultimately in the function position is either a variable or a term annotated with its type.

Reduction Rules

(λy↦t : (x:S)→T) s ↝ t[s:S / y] : T[s:S / x]

(t : T) ↝ t

The substitution operation t[e / x] replaces every occurrence of the variable x with the elimination e, avoiding name capture. To form an application that can reduce, a lambda term must be annotated by its type to make an elimination. The type annotation gives the lambda-abstraction a kind of "reactivity", allowing application to proceed. Once we reach the point where no more application is happening and the active t : T is being embedded back into the term syntax, we can drop the type annotation.

Let's extend the ↝ reduction relation by structural closure: the rules apply anywhere inside terms and eliminations that you can find something matching the left-hand side. Write ↝* for the reflexive-transitive (0-or-more-step) closure of ↝. The resulting reduction system is confluent in this sense:

If s ↝* p and s ↝* q, then there exists some r such that p ↝* r and q ↝* r.

Contexts

Context   ::=     |   Context, Var : Term

Contexts are sequences which assign types to variables, growing on the right, which we think of as the "local" end, telling us about the most recently bound variables. An important property of contexts is that it's always possible to choose a variable not already used in the context. We maintain the invariant that the variables ascribed types in the context are distinct.

Judgments

Judgment   ::=   Context ⊢ Term has Term   |   Context ⊢ Elim is Term

That's the grammar of judgments, but how to read them? For a start, ⊢ is the tradional "turnstile" symbol, separating assumptions from conclusions: you can read it informally as "says".

G ⊢ T has t

means that given context G, type T admits term t;

G ⊢ e is S

means that given context G, elimination e is given type S.

Judgments have interesting structure: zero or more inputs, one or more subject, zero or more outputs.

INPUTS                   SUBJECT        OUTPUTS
Context |- Term   has    Term
Context |-               Elim      is   Term

That is, we must propose the types of terms in advance and just check them, but we synthesize the types of eliminations.

Typing Rules

I present these in a vaguely Prolog style, writing J -: P1; ...; Pn to indicate that judgment J holds if premises P1 through Pn also hold. A premise will be another judgment, or a claim about reduction.

Terms

G ⊢ T has t   -:   T ↝ R;   G ⊢ R has t

G ⊢ * has *

G ⊢ * has (x:S)→T   -:   G ⊢ * has S;   G, z:S !- * has T[z / x]

G ⊢ (x:S)→T has λy↦t   -:   G, z:S ⊢ T[z/x] has t[z/y]

G ⊢ T has (e)   -:   G ⊢ e is T

Eliminations

G ⊢ e is R   -:   G ⊢ e is S;   S ↝ R

G, x:S, G' ⊢ x is S

G ⊢ f s is T[s:S / x]   -:   G ⊢ f is (x:S)→T;   G ⊢ S has s

And that's it!

Only two rules are not syntax-directed: the rule which says "you can reduce a type before you use it to check a term" and the rule which says "you can reduce a type after you've synthesized it from an elimination". One viable strategy is to reduce types until you've exposed the topmost constructor.

This system is not strongly normalizing (because of Girard's Paradox, which is a liar-style paradox of self-reference), but it can be made strongly normalizing by splitting * into "universe levels" where any values which involve types at lower levels themselves have types at higher levels, preventing self-reference.

This system does, however, have the property of type preservation, in this sense.

If G ⊢ T has t and G ↝* D and T ↝* R and t ↝ r, then D ⊢ R has r.

If G ⊢ e is S and G ↝* D and e ↝ f, then there exists R such that S ↝* R and D ⊢ f is R.

Contexts can compute by allowing the terms they contain to compute. That is, if a judgment is valid now, you can compute its inputs as much as you like and its subject one step, and then it will be possible to compute its outputs somehow to make sure the resulting judgment stays valid. The proof is a simple induction on typing derivations, given the confluence of -->*.

Of course, I've presented only the functional core here, but extensions can be quite modular. Here are pairs.

Term   ::=   ...   |   (x:S)*T   |   s,t

Elim   ::=   ...   |   e.head   |   e.tail

(s,t : (x:S)*T).head ↝ s:S

(s,t : (x:S)*T).tail ↝ t:T[s:S / x]

G ⊢ * has (x:S)*T   -:   G ⊢ * has S;   G, z:S ⊢ * has T[z / x]

G ⊢ (x:S)*T has s,t   -:   G ⊢ S has s;   G ⊢ T[s:S / x] has t

G ⊢ e.head is S   -:   G ⊢ e is (x:S)*T

G ⊢ e.tail is T[e.head / x]   -:   G ⊢ e is (x:S)*T

Answer 3

The Curry-Howard correspondence says that there is a systematic correspondence between type systems and proof systems in logic. Taking a programmer-centric view of this, you could recast it this way:

• Logical proof systems are programming languages.
• These languages are statically typed.
• The type system's responsibility in such a language is to forbid programs that would construct unsound proofs.

Seen from this angle:

• The untyped lambda calculus that you summarize doesn't have a significant type system, so a proof system built on it would be unsound.
• The simply typed lambda calculus is a programming language that has all the types necessary to build sound proofs in sentential logic ("if/then", "and", "or", "not"). But its types aren't good enough to check proofs that involve quantifiers ("for all x, ..."; "there exists an x such that ...").
• Dependently typed lambda calculus has types and rules that support sentential logic and first-order quantifiers (quantification over values).

Here are the rules of natural deduction for first-order logic, using a diagram from the Wikipedia entry on natural deduction. These are basically the rules of a minimal dependently typed lambda calculus as well.

Note that the rules have lambda terms in them. These can be read as the programs that construct the proofs of the sentences represented by their types (or more succinctly, we just say programs are proofs). Similar reduction rules that you give can be applied to these lambda terms.

---

Why do we care about this? Well, first of all, because proofs may well turn out to be a useful tool in programming, and having a language that can work with proofs as first-class objects opens many avenues. E.g., if your function has a precondition, instead of writing it down as a comment you can actually demand a proof of it as an argument.

Second, because the type system machinery needed to handle quantifiers may have other uses in a programming context. In particular, dependently typed languages handle universal quantifiers ("for all x, ...") by using a concept called dependent function types—a function where the static type of the result can depend on the runtime value of the argument.

To give a very pedestrian application of this, I write code all the time that has to read Avro files that consist of records with uniform structure—all share the same set of field names and types. This requires me to either:

1. Hardcode the structure of the records in the program as a record type.
   • Advantages: The code is simpler and the compiler can catch errors in my code
   • Disadvantage: The program is hardcoded to read files that agree with the record type.
2. Read the schema of the data at runtime, represent it generically as a data structure, and use that to process records generically
   • Advantages: My program is not hardcoded to just one file type
   • Disadvantages: The compiler can't catch as many errors.

As you can see in the Avro Java tutorial page, they show you how to use the library according to both of these approaches.

With dependent function types you can have your cake and eat it, at the cost of a more complex type system. You could write a function that reads an Avro file, extracts the schema, and returns the file's contents as a stream of records whose static type depends on the schema stored in the file. The compiler would be able to catch errors where I, for example, tried to access a named field that might not exist in the records of the files that it'll process at runtime. Sweet, huh?