A Relational Solver for Constraint-based Type Inference

TL;DR

This paper introduces a miniKanren-based type inference system for an untyped educational language featuring first-class functions, pattern matching, and polymorphism, addressing unique challenges through specialized techniques.

Contribution

It presents a novel relational solver tailored for a complex, untyped language, incorporating optimizations for polymorphic and recursive types within miniKanren.

Findings

Successfully implemented a type inferencer in miniKanren

Handled polymorphic and recursive types effectively

Enhanced inference performance with specific tricks

Abstract

We present a miniKanren-based type inferencer for an educational programming language with first-class functions, S-expressions, and pattern-matching. The language itself is untyped which adds a certain specificity to the problem and requires the employment of techniques conventionally used in implicit/gradual typing settings. The presence of polymorphic and recursive types poses a certain challenge when implementing the inferencer in miniKanren and requires a number of tricks, optimizations, and extensions to be used; we report on those as well.