English

A Relational Solver for Constraint-based Type Inference

Programming Languages 2024-09-02 v1

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.

Keywords

Cite

@article{arxiv.2408.17138,
  title  = {A Relational Solver for Constraint-based Type Inference},
  author = {Eridan Domoratskiy and Dmitry Boulytchev},
  journal= {arXiv preprint arXiv:2408.17138},
  year   = {2024}
}
R2 v1 2026-06-28T18:28:36.047Z