31
$\begingroup$

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?

$\endgroup$

migrated from stackoverflow.com Nov 23 '15 at 19:04

This question came from our site for professional and enthusiast programmers.

  • 4
    $\begingroup$ The rules of Pure Type Systems are very brief. Simply Easy is about implementing dependent types. $\endgroup$ – pigworker Nov 10 '15 at 22:56
  • 2
    $\begingroup$ So it is not "hostile" in the sense of offensive, but in the sense you think I'm demanding a lot for not showing enough effort in finding the answer by myself? If that is the case, I agree this question might be demanding a lot so maybe it is just bad. But there is also a lot of effort behind it, do you think I should edit in my attempts? $\endgroup$ – MaiaVictor Nov 10 '15 at 22:57
  • 3
    $\begingroup$ I'm offended, too, on behalf of my coauthors who wrote the text of "A Tutorial Implementation of a Dependently Typed Lambda Calculus", which replaced "Simply Easy" as a working title. I wrote the kernel of the code, which is a typechecker in <100 lines of Haskell. $\endgroup$ – pigworker Nov 10 '15 at 23:01
  • 2
    $\begingroup$ Then I certainly expressed myself badly. I love the "Simply Easy" paper and am reading it in every break since a few days ago - it is the only thing it in the world that gave me a partial sensation I'm starting to understand the subject (and believe I tried). But I do think it is aimed at a public with more knowledge than I have, and that could be why I'm still having some trouble getting part of it. Nothing to do with the quality of the paper, but my own limitations. $\endgroup$ – MaiaVictor Nov 10 '15 at 23:06
  • 1
    $\begingroup$ @pigworker and the code is my favorite part of it, exactly because it (in relation to the english explanation) is a much shorter, yet complete, explanation of the whole, as I asked here. Do you happen to have a copy of the code I can download? $\endgroup$ – MaiaVictor Nov 10 '15 at 23:24
7
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ Seconding "Simpler, Easier". $\endgroup$ – András Kovács Nov 11 '15 at 6:49
  • $\begingroup$ The first reduction rule on forall looks weird. Unlike lambdas, foralls should not be applied in a well-typed way (right?). $\endgroup$ – chi Nov 11 '15 at 9:09
  • $\begingroup$ @chi, I don't understand what you're saying. Perhaps my notation is bad: the reduction rule says (λ v. b ∈ ∀ (v : σ). τ) (t ∈ σ) ~> SUBS(b, v, t) ∈ SUBS(τ, v, t). $\endgroup$ – user3237465 Nov 11 '15 at 9:27
  • 1
    $\begingroup$ I find the notation misleading. It looks as if you had two rules: one for the nonsense (∀ (v : σ). τ) t ~> ... an another for the meaningful (λ v. b) t ~> .... I would remove the first, and turn it into a comment below. $\endgroup$ – chi Nov 11 '15 at 9:33
  • 1
    $\begingroup$ Rule (1) contains its conclusion as a premise. You can compare the simplicity of your system to the bidirectional version only once you have a system which works. You may say you keep everything normalized, but your rules don't. $\endgroup$ – pigworker Nov 11 '15 at 10:39
24
$\begingroup$

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

$\endgroup$
  • 1
    $\begingroup$ G, x:S, G' ⊢ x is S -: G' ⊬ x? $\endgroup$ – user3237465 Nov 11 '15 at 9:30
  • 1
    $\begingroup$ @user3237465 Nope. Thanks! Fixed. (When I was replacing ascii art turnstiles with html turnstiles (thus making them invisible on my phone; sorry if that's happening elsewhere) I missed that one.) $\endgroup$ – pigworker Nov 11 '15 at 9:47
  • 1
    $\begingroup$ Oh, I thought you were just pointing out the typo. The rule says that, for each variable in the context, we synthesize the type that the context assigns it. When introducing contexts, I said "We maintain the invariant that the variables ascribed types in the context are distinct." so shadowing is disallowed. You'll see that every time the rules extend the context, they always choose of a fresh "z" which instantiates whatever binders we're stepping under. Shadowing is anathema. If you have context x : *, x : x then the type of the more local x is no longer ok because it's the x out of scope. $\endgroup$ – pigworker Nov 11 '15 at 10:09
  • 1
    $\begingroup$ I just wanted you and the other answerers to know that I'm coming back to this thread every break from work. I really want to learn this, and for the first ime I fell like I actually get most of it. The next step will be implementing and writing a few programs. I'm delighted to be able to live in an era where information about such wonderful topics are available across the globe to someone like me, and that is all thanks to geniuses like you who dedicate some time of their life to spread that knowledge, for free, on the internet. Sorry again for phrasing my question badly, and thank you! $\endgroup$ – MaiaVictor Nov 11 '15 at 22:27
  • 1
    $\begingroup$ @cody Yes, there is no expansion. To see why it's not necessary, note that the two computation rules allow you to deploy the strategy where you normalize types completely before you check terms, and you also normalize types immediately after synthesizing them from eliminations. So in the rule where the types must match, they are already normalized, hence equal on the nose if the "original" checked and synthesized types were convertible. Meanwhile, restricting equality checks to that place only is ok because of this fact: if T is convertible to a canonical type, it reduces to a canonical type. $\endgroup$ – pigworker Sep 1 '16 at 9:18
8
$\begingroup$

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.

First-order natural deduction

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?

$\endgroup$
  • 1
    $\begingroup$ Building types at runtime in the fashion you mentioned is something really cool I haven't thought about. Rather sweet, indeed! Thanks for the insightful answer. $\endgroup$ – MaiaVictor Nov 11 '15 at 22:33

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.