Type checking through unification

TL;DR

This paper introduces a novel approach to type checking in dependently typed languages by encoding the process as higher-order unification constraints, simplifying the implementation and leveraging existing unification algorithms.

Contribution

It presents an algorithm that integrates type checking and unification, reducing complexity by encoding type checking as unification constraints.

Findings

Reduces type-checking complexity in dependently typed languages.

Leverages existing higher-order unification algorithms.

Provides a unified framework for type checking and unification.

Abstract

In this paper we describe how to leverage higher-order unification to type check a dependently typed language with meta-variables. The literature usually presents the unification algorithm as a standalone component, however the need to check definitional equality of terms while type checking gives rise to a tight interplay between type checking and unification. This interplay is a major source of complexity in the type-checking algorithm for existing dependently typed programming languages. We propose an algorithm that encodes a type-checking problem entirely in the form of unification constraints, reducing the complexity of the type-checking code by taking advantage of higher order unification, which is already part of the implementation of many dependently typed languages.