A Relational Solver for Constraint-based Type Inference

on YouTube ↗17m

" summary

A miniKanren-based type inferencer for the Lama educational language is implemented: it infers constraints from terms, solves them relationally, and applies substitutions to produce types; the system supports polymorphic and explicit recursive types by adding non-relational primitives like occurs-check hooks and a bind-hook primitive to register solutions on demand. The prototype typechecks the majority of compiler tests but shows exponential blowup for S-expression containment constraints (one test hits ~20s) and emits verbose recursive types; results are preliminary and optimizations partially mitigate the cost.

AI-written summary · about

" chapters (13)

1. 0:00Introduction
2. 1:05Relational programming approach
3. 2:27Lama language type system
4. 3:11Constraint syntax and satisfaction
5. 4:42Relational optimizations
6. 6:06Logic variables and substitutions
7. 7:56Constraints and constructor forms
8. 8:58Hook-based recursive types
9. 10:45Recursive type handling
10. 11:28Constraint ordering and performance
11. 12:30Evaluation with L compiler
12. 14:17Results and future research
13. 15:03Q&A