Simply-typed Lambda Calculus [Part 1]

Added: May 29, 2025 by mutkach

Plan and current state:

1. Follow the Ocaml type checker implementation from Types and Programming Languages by Benjamin Pierce [Done]
2. Write a Haskell type checker implementation based on the Ocaml implementation from the book [Done]
3. Write a Rust type checker implementation based on the Haskell implementation [Done]
4. Write a PEG in Pest to parse strings into ASTs. [Done]
5. Write a REPL using rustyline [to be done]

You can follow the project along on github

For a long time I wanted to get into type theory. One of the classics in this genre is of course the Types and Programming Languages by Benjamin Pierce (also one of the creators of the Program Verification course). To be honest, type theory is something that lies very closely to Logic rather than any other familiar parts of Mathematics. And “studying” Logic is quite tedious. Some of my mathematician friends share that opinion. It’s difficult to say what is exactly so tiring when studying logic - it is just “not quite my tempo”. Something changed in me when I first saw the Ocaml implementation of the type checking algorithm for simple types and trivial terms (no “let” bindings, no operations, but still…). I was looking at tiny piece of code that was clear as a glass and readable as a road sign (forgive me for that little poetic outburst…) What I gathered is at least a little part of the Type theory is just chewing through some very simple ideas. But, mind you, that is literally the beginning - the real type systems will appear afterwards. But still, some simple ideas may hide behind some very verbose and redundant language but become clear in code. That is one of such cases.

However. Once I got the type checker running - I wanted more. Now I want a sort of a playground where I could try out different type systems and work with them interactively. Maybe one day, dependent typing will become approachable too. Anyways in order to create such a playground, the type checker would be the lesser part. First, I want to have a working parser so that I could type expressions in “mathematical” notation and not as nested ASTs typed down by hand! For that matter we have Pest - it is a simple PEG (Parser Expression Generator) that takes as an input a sort of a grammar expression and then proceeds to “generate” a Parser of that grammar for you. There was one thing that I appreciated a lot - it was that little interactive WYSIWYG window on its site page where you could literally type in the grammar and see the parsed tree (or lack thereof, too).

From here I will proceed onwards with PEG parsing and REPL creation.

Here’s some a small piece of code that does checking for abstraction and application types for you:

 1Term::TAbstraction(abs) => {
 2    let (variable_name, term) = abs.to_owned();
 3    let Ok(term_type) = self.check_type(&term) else {
 4        return Err("Bad abstraction type!");
 5    };
 6    let Some(index) = self.get_idx_from_name(&variable_name) else {
 7        return Err("No such binding found!");
 8    };
 9    let Some(variable_type) = self.get_type_from_idx(index) else {
10        return Err("Bad type");
11    };
12    Ok(TType::TFun(Box::new((variable_type, term_type))))
13}
14Term::TApplication(app) => {
15    let (lambda, arg) = *app.to_owned();
16    let Ok(lambda_type) = self.check_type(&lambda) else {
17        return Err("Bad lambda type!");
18    };
19    let Ok(arg_type) = self.check_type(&arg) else {
20        return Err("Bad argument type");
21    };
22    match lambda_type {
23        TType::TFun(fun) => {
24            let (from, to) = *fun;
25            if from == arg_type {
26                Ok(to)
27            } else {
28                Err("Lambda argument mismatch")
29            }
30        }
31        _ => Err("Wrong lambda type"),
32    }
33}

Here’s - not a piece - but the whole type-checker written in Haskell:

 1checkType :: Context -> Term -> MyType
 2checkType ctx t = case t of
 3  TermIf if' then' else' ->
 4    let ifType = checkType ctx if' in 
 5    let thenType = checkType ctx then' in 
 6    let elseType = checkType ctx else' in 
 7    case (ifType, thenType, elseType) of
 8                  (TBool, a, b) -> if a == b then a else error "Diverging arms of IF!"
 9                  _ -> error "Not a boolean"
10  TermFalse -> TBool
11  TermTrue -> TBool
12  TermAbst name term' -> 
13    let index = getIndexFromName ctx name in
14    let variableType = getTypeFromIndex ctx index in
15    let termType = checkType ctx term' in
16    TFun variableType termType
17  TermApp lambda arg ->
18    let argType = checkType ctx arg in 
19    let lambdaType = checkType ctx lambda in 
20    case lambdaType of
21              (TFun from to) -> if argType == from then to else error "Bad argument"
22              _ -> error "Wrong lambda type"
23  TermVar index'-> getTypeFromIndex ctx index'

Looks great. By the way, maybe I should stick to Haskell?