[miniKanren24] A Relational Solver for Constraint-based Type Inference

A Relational Solver for Constraint-based Type Inference (Video, Minikanren 2024)
Dmitri Boulytchev, and Eridan Domoratskiy
(Saint Petersburg State University; ITMO University)
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.
Presentation at the Minikanren 2024 workshop, Sept 6, 2024, icfp24.sigplan...
Sponsored by ACM SIGPLAN,