A Type Checking Algorithm for Higher-rank, Impredicative and Second-order Types

TL;DR

This paper presents a sound type checking algorithm for a complex subclass of functional programs with advanced type features, requiring minimal annotations and extending to pattern matching and let-bindings.

Contribution

It introduces a novel type checking algorithm for higher-rank, impredicative, and second-order types, with proven soundness and practical implementation.

Findings

Algorithm successfully type checks complex functional programs

Prototype implementation demonstrates practical viability

Soundness established with respect to System Fω

Abstract

We study a type checking algorithm that is able to type check a nontrivial subclass of functional programs that use features such as higher-rank, impredicative and second-order types. The only place the algorithm requires type annotation is before each function declaration. We prove the soundness of the type checking algorithm with respect to System $\mathbf{F}_{\omega}$, i.e. if the program is type checked, then the type checker will produce a well-typed annotated System $\mathbf{F}_{\omega}$ term. We extend the basic algorithm to handle pattern matching and let-bindings. We implement a prototype type checker and test it on a variety of functional programs.