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.