elab-stlc-bidirectional

Bidirectional type checking for a simply typed lambda calculus

Bidirectional typing is a technique for implementing type checking and elaboration, allowing type annotations to be provided when checking terms to help to disambiguate terms. It is used in the implementation of many dependent and non-dependently typed programming languages, for example in Idris, Agda, Haskell, Scala, Typescript, etc.

This project implements an elaborator for a simply typed lambda calculus with booleans and integers. We use bidirectional type checking during elaboration to allow the programmer to omit some type annotations, breaking elaboration into two mutually recursive functions:

val elab_check : context -> tm -> Core.ty -> Core.tm
val elab_infer : context -> tm -> Core.tm * Core.ty

A similar approach is used in later projects, like elab-dependent and elab-record-patching to implement more complicated type systems with dependent types and subtyping.

Project overview

Module	Description
Main	Command line interface
Lexer	Lexer for the surface language
Parser	Parser for the surface language
Surface	Surface language, including elaboration
Core	Core language, including normalisation, and pretty printing
Prim	Primitive operations

Resources

• David R. Christiansen, Bidirectional Typing Rules: A Tutorial
• David R. Christiansen, Bidirectional Type Checking
• Jana Dunfield and Neel Krishnaswami, Bidirectional Typing
• Frank Pfenning, Lecture Notes on Bidirectional Type Checking
• Conor McBride, Type Inference Needs a Revolution

Examples

$ stlc-bidirectional elab <<< "fun x => x + 2"
<input>:1:4: ambiguous parameter type
[1]

$ stlc-bidirectional elab <<< "fun (x : Int) => x + 2"
fun (x : Int) => #int-add -x 2 : Int -> Int

$ stlc-bidirectional elab <<< "(fun x f => f x * x) : Int -> (Int -> Int) -> Int"
fun (x : Int) => fun (f : Int -> Int) => #int-mul -(f x) x :
  Int -> (Int -> Int) -> Int

More examples can be found in tests.t.