Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis

TL;DR

This paper introduces a proof-relevant Horn clause calculus that automates type inference and term synthesis in dependently typed languages, ensuring decidability and soundness.

Contribution

It presents a novel calculus translating dependent type inference and synthesis into proof-relevant Horn clause logic, enabling automated reasoning.

Findings

Decidability of the proposed method is proven.

Soundness of the approach is established.

The calculus effectively automates type inference and term synthesis.

Abstract

First-order resolution has been used for type inference for many years, including in Hindley- Milner type inference, type-classes, and constrained data types. Dependent types are a new trend in functional languages. In this paper, we show that proof-relevant first-order resolution can play an important role in automating type inference and term synthesis for dependently typed languages. We propose a calculus that translates type inference and term synthesis problems in a dependently typed language to a logic program and a goal in the proof-relevant first-order Horn clause logic. The computed answer substitution and proof term then provide a solution to the given type inference and term synthesis problem. We prove the decidability and soundness of our method. The paper is under consideration for acceptance in TPLP.