Bidirectional Type Checker in Scheme

This project is an implementation of the algorithmic system described in Section 3 of "A Mechanical Formalization of Higher-Ranked Polymorphic Type Inference".

Usage

You will need a Scheme implementation that supports R6RS and the format procedure. This project was developed in Chez Scheme (Version 10.4.1).

To use this project, load the main.scm file directly into your Scheme environment/REPL.

Expressions, Types, and Judgements

The implementation contains procedures for constructing expressions and types. Here are some examples:

Expression (Haskell)	Representation
42	(Expr.Int 42)
id	(Expr.Var "id")
\x -> x	(Expr.Lam (Expr.Var "x") (Expr.Var "x"))
(\x -> x) 42	(Expr.App (Expr.Lam (Expr.Var "x") (Expr.Var "x")) (Expr.Int 42))
id :: Int -> Int	(Expr.Ann (Expr.Var "id") (Type.Arr Type.Int Type.Int))

Type (Haskell)	Representation
Int	Type.Int
a	(Type.Var "a")
Int -> Int	(Type.Arr Type.Int Type.Int)
forall a. a -> a	(Type.Forall (Type.Var "a") (Type.Arr (Type.Var "a") (Type.Var "a")))

Judgement	Representation
x : A	(Judgement.Bind x A)
A <: B	(Judgement.Sub A B)
e <= A	(Judgement.Check e A)
e =>_a w	(Judgement.Infer e a w)
A * e =>_a w	(Judgement.App A e a w)
id =>_a (a <: Int -> Int)	(Judgement.Infer id a (Judgement.Check a (Type.Arr Type.Int Type.Int)))

Worklists

Worklists are represented as plain lists. The head of the list is the top of the worklist, while the tail is the rest.

Worklist	Representation
|- (\x -> x) 42 <= Int	[(Judgement.Check (Expr.App id (Expr.Int 42)) Type.Int)]
+ : Int -> Int -> Int |- + 4 2 <= Int	[(Judgement.Check addFourTwo Type.Int) (Judgement.Bind (Expr.Var "add") (...))]