Bidirectional typechecking with dependent typing

I have to admit this is an another thing that's everybody has been pushing at me and I have been disregarding it foolishly. This time I catched on.

Bidirectional typechecking is cool. I'm going to show you an appetizer.

Case of simply typed lambda calculus

Everybody has stumbled across lambda calculus and knows it inside-outside by now.

These formation rules you may have seen many times by now. If not I'll explain what they mean in a moment.

x free in Γ     A type
────────────────────── (var)
Γ, x : A ⊢ x : A

Γ, x : A ⊢ y : B
──────────────── (Iλ)
Γ ⊢ λx.y : A → B

Γ ⊢ f : A → B     Γ ⊢ a : A
─────────────────────────── (Eλ)
Γ ⊢ f a : B

Every rule here forms from a line with stuff over and under it.

If the things above the line are true, then the thing under the line is true as well.
The ⊢ has scope on the left side and expression on the right side. If an expression is true, you can form that kind of an expression.
Γ is a scope consisting of variables and their types.
The e : T is a typing judgement. The expression e on the left side is treated as if it had some type T.

You could encode the formation rules in Haskell like this:

data Term =
      Var Int
    | Abs Term
    | App Term Term

data Type =
      Some Int
    | Arrow Type Type

This would let you write terms and then deduce types for them. To do that you implement a small fragment of μKanren and use it to express the formation rules.

inference :: Type -> [Type] -> Type -> Goal
inference (Var i) scope t =
    eq (scope !! i) t
inference (Abs body) scope t = fresh2 goal where
    goal a b = inference body (a:scope) b ∧ eq t (Arrow a b)
inference (App fn arg) scope t = fresh goal where
    goal a = inference arg scope a ∧ inference fn scope (Arrow a t)

In programming we enjoy type inference as it makes programming easier. The inferencer figures out which types are needed to run the program.

One problem though.

Proofs ≃ programs.
Propositions ≃ types.

To understand this, look at the formation rules. They contain everything that was needed to form the program. Look at this for instance:

──────── var   ──────── var
y, x ⊢ x       y, x ⊢ y
─────────────────────── Eλ   ────────── var
y, x ⊢ x y                   y, z ⊢ z
─────────────────────── Iλ   ────────── Iλ
y ⊢ (λx.x y)                 y ⊢ (λz.z) 
─────────────────────────────────────── Eλ
y ⊢ (λx.x y)(λz.z)

You can just take the lowest proposition here and build the rest of this proof from it.

What is being proved in the above proposition?

───────────── var ─ var
A → A ⊢ A → A     A
─────────────────── Eλ   ───── var
A, (A → A) ⊢ A           A ⊢ A
─────────────────── Iλ   ───── Iλ
A ⊢ (A → A) → A          A → A
────────────────────────────── Eλ
A ⊢ A

The proposition says: Assuming A is true, then A is true.

Normalize the expression and it's easier to see:

y ⊢ (λx.x y)(λz.z)
y ⊢ (λz.z)y
y ⊢ y

Indeed it says such a simple thing.

When we take these ideas further, we end up with propositions that say more interesting things. Things such as:

Given a graph and a target point in graph, then any other point 'n' in graph, you can either have the path with the shortest distance to target point, or then the target node is unreachable from that point 'n'. (proof: Dijikstra's algorithm)
Addition between natural numbers is commutative. (an inductive proof can be built from pieces)
Variable-length quantity is a byte sequence where the highest most significant bits are set, until the last byte that has highest most significant bit cleared. Natural numbers are isomorphic with VLQ-values. (proof: Encoding/Decoding of VLQ-values)

Proof-checking fails if the proof doesn't satisfy the proposition.

If we look at Hindley-Milner type inference under these ideas, it seems to do something rather nonsensical. It's trying to find propositions that satisfy a proof. Instead of type-inference you'd likely want to program-inference. Or maybe just assistance for writing programs.

If you think about the content of these propositions here, you'd likely want to write such propositions because they verify that your program is doing what you expect from it.

So most likely when you're writing a proof, you already have some proposition you work towards proving. Bidirectional typechecking lets you work with this kind of basis.

Bidirectional typechecking

When building a bidirectional typechecker, we re-examine and then re-group the formation rules.

Some rules become justifications and end up being marked with down-arrow:

── (var)
A↓

A → B↓     A↑
───────────── (Eλ)
B↓

Other rules become verifications and mark with up-arrows:

B↑
────── (Iλ)
A → B↑

Additionally we may use justifications to produce verifications:

A↓
── (↑↓)
A↑

If we transition this back to Haskell, we get the following structures:

data Neutral =
      Var Int
    | App Neutral Normal

data Normal =
      Abs Normal
    | Neutral Neutral

data Type =
      Some Int
    | Arrow Type Type

We can reuse existing naming. Verifications are normal-forms and justifications are neutral-forms of lambda calculus.

Typechecking programs falls out from the typechecking rules:

infer :: [Type] -> Neutral -> Either Fail Type
infer ctx (Var x) =
    Right (ctx !! x)
infer ctx (App f x) = do
    (a, b) <- infer ctx f >>= check_arrow
    check ctx x a
    return b

check :: [Type] -> Normal -> Type -> Either Fail ()
check ctx (Abs body) ty = do
    (a, b) <- check_arrow ty
    check (a:ctx) body b
check ctx (Neutral n) ty = do
    t <- infer ctx n
    if ty == t then Right () else Left (NotEqual ty t)

check_arrow (Arrow a b) = Right (a,b)
check_arrow a           = Left (NotArrow a)

Annotated structures

Sometimes the following kind of structure is described in neutral forms:

Ann Normal Type

It adds the following kind of rule into infer

infer ctx (Ann t ty) = do
    check ctx t ty
    return ty

Annotations allow you to build reducible expressions. If the bidirectional typing has been done well, you can write the reduction algorithms such that they cannot be triggered without correct type information.

β-redex: App (Ann (Abs f) (Arrow a b)) x
    ---> Ann (apply f (Ann x a)) b

This means that the type-information can completely determine how any such redex is reduced. Under bidirectional typing meaning of any redex can be overloaded without compiling programs to categories.

You don't necessarily need the Ann rule if you store every expression as a normal-form. The rest of the code presented assumes the Ann -rule is included.

Normalization

Shake the inference rules vigorously enough and even the normalization algorithm falls to your hand.

nf :: Normal -> Normal
nf = nof where
    nef :: Neutral -> Normal
    nof :: Normal  -> Normal
    nef (Var i)   = Neutral (Var i)
    nef (App a b) = apply (nef a) (nof b)
    nef (Ann a _) = nof a
    nof (Neutral a) = nef a
    nof (Abs a)     = Abs (nof a)

apply :: Normal -> Normal -> Normal
apply (Neutral n) b = (Neutral (App n b))
apply (Abs a) b = substitute a b

substitute :: Normal -> Normal -> Normal
substitute a v = (s_nf 0 v a) where
    s_nf i v (Neutral n) = s_sp i v n
    s_nf i v (Abs a) = Abs (s_nf (i+1) v a)
    s_sp i v (Var j) | i == j    = wknf i 0 v
                     | otherwise = Neutral (Var j)
    s_sp i v (App s n) = apply (s_sp i v s) (s_nf i v n)
    wknf k p (Neutral n) = Neutral (wksp k p n)
    wknf k p (Abs n) = Abs (wknf k (p+1) n)
    wksp k p (Var i) | (p <= i)  = (Var (i+k))
                     | otherwise = (Var i)
    wksp k p (App a b) = App (wksp k p a) (wknf k p b)

Well actually it's not so straightforward. You may find some bugs in the above program.

If you want to know how to do it properly, I wrote this after reading Keller-Altenkirch 2010 paper: "Hederitary Substitutions for Simple Types, Formalized"

Correctly written in Agda, the above program would form a proof of termination for simply typed lambda calculus through an induction to the formation rules. How it's achieved is incredibly clever and relies on the fact that the formation rules in lambda calculus have are locally complete and sound.

The program I wrote can be run for a badly-typed fragment that will cause it to get stuck. I've broken it by not η-expanding variables and having the Neutral n -rule in the program that does a suspension for the application.

If the elimination rules can be applied such that the original proposition can be reconstituted from them, then they have local completeness. Local soundness means that additional information cannot be derived from what is put in at introduction rules. Check Pfenning's course material in the end to read more about this.

For lambdas we can do this kind of rule to present that functions rules are locally complete:

M : x → y
M = λx.Mx

Now if you were to apply this into every variable in a well-typed lambda expression, you will ensure that every non-normal function call eventually forms a beta-redex. The apply-function no longer gets anything else but functions. It becomes possible to prove through induction that it terminates. Eg. The Neutral... -rule in apply -function can be left out.

Case of dependent typing

To start typechecking dependently typed programs, we just need to drop the separate type terms, then introduce universes and ∏-types.

data Neutral =
      Var Int
    | App Neutral Normal
    | Ann Normal Normal

data Normal =
      Abs Normal
    | Pi Normal Normal
    | Neutral Neutral
    | Universe Int

The β-redex changes accordingly:

β-redex: App (Ann (Abs 'x' f) (Pi 'x' a b)) x
     --> Ann f[x := Ann x a] b[x := Ann x a]

In the typechecking we need to replace check_arrow with check_pi. The apply needs to substitute the value into the type. Then few new rules need to be written.

infer :: [Normal] -> Neutral -> Either Fail Normal
infer ctx (Var x) =
    Right (ctx !! x)
infer ctx (App f x) = do
    (a, b) <- infer ctx f >>= check_pi
    check ctx x a
    return (substitute b x)
infer ctx (Ann t ty) = do
    check ctx t ty
    return ty

check :: [Normal] -> Normal -> Normal -> Either Fail ()
check ctx (Abs body) ty = do
    (a, b) <- check_pi ty
    check (a:ctx) body b
check ctx (Neutral n) ty = do
    t <- infer ctx n
    if ty == t then Right () else Left (NotEqual ty t)
check ctx (Universe k) ty | universe_of k ty = Right ()
                          | otherwise        = Left (NotUniverse k ty)
check ctx (Pi a b) ty = do
    check ctx a ty
    check (a:ctx) b ty

check_pi (Pi a b) = Right (a,b)
check_pi a        = Left (NotPi a)

universe_of i (Universe j) | i < j = True
universe_of i ty                   = False

Now if user gives you a proposition, you will check that it's a valid type:

check proposition (Universe k)

When she gives a proof for the proposition, you will check that the proof is valid for the proposition:

check proof proposition

Shareware version, purchase with education

What I shown here is just an appetizer. To really understand what's going on, watch&read Frank Pfenning's 15-317 Constructive Logic -course. There's also Roy Dickhoff's "Some remarks on proof-theoretic semantics" that helps understand some details when it comes recognizing whether a rule is a verification or justification.