A Relational Solver for Constraint-based Type Inference

We present preliminary results on using relational programming for implementing type inference for a realistic programming language with first-class functions, S-expressions, and pattern-matching. This language, LaMa, has been used for a few years as an educational language to teach compiler construction courses in a number of universities. While not quite being the production-tier programming language, LaMa still is rich enough to, first, demonstrate the majority of relevant techniques in compiler construction domain, and, second, to implement its own compiler. An important feature of LaMa is the lack of a type system. This brings in all well-known advantages and drawbacks. The motivation for this work was to soften the latter by providing an automatic tool to discover inconsistencies in LaMa programs caused by incoherent usage of data, which is conventionally done by means of a type system. In a nutshell, in our approach a set of constraints is extracted from a program, and the objective is to check if this set of constraints is consistent. While constraint extraction is done in a conventional syntax-directed way and implemented in a functional language, the consistency check is performed relationally. However, as a naïve relational implementation does not perform well, a number of refinements, optimizations and extensions to the vanilla miniKanren needs to be applied. In the talk we give an overview of LaMa programming language, devised type system, relational type inference approach, and describe various refinement of vanilla relational solver. (Совместная работа с Д.Ю. Булычевым.)
Рабочая (необработанная) запись на RuTube-канале (https://rutube.ru/video/8595125da2a8f7dab94058e3e4212ca1/) ИСИ СО РАН. Есть презентация доклада (https://persons.iis.nsk.su/files/persons/pages/domoratskiy10dec24.pdf).