Type Checking

Reading

• Typechecker Zoo

  In particular Algorithm W was the first implemented algorithm for function-level type inference.

  I intend to implement a form of System Fω.

• Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism

• Rust

  Rust uses a form of System Fω with Bidirectional typechecking implemented using a unification (union-find) algorithm.

  See rustc_hir_analysis, ena (docs.rs)