miniKanren Philosophy
summary
Description of a logic language with a tiny core: a few primitives (fresh, unification, disequality, conde) let relations replace functions and let queries run backwards to generate inputs. A probabilistic chooser conP (≈40 lines) biases generation so the type-inference fuzzer produces 1,000+ richer programs instead of trivial constants, which surfaces a real bug in the type inferencer. Implemented quine and twine generators succeed; some demo fixes remain outstanding.
AI-written summary · about
chapters (19)
- 0:00Intro
- 1:00Symbols
- 2:00Control Operators
- 3:00Underscores
- 4:00Run
- 5:00Program
- 16:00Fix
- 17:00Inference
- 19:00Type
- 21:00Type Inference
- 23:00Well Type
- 26:00Floating Point Numbers
- 27:00Interpreter
- 29:00Applications
- 31:00Natto
- 32:00Holloway
- 33:00Dont tell them
- 34:00QQ
- 37:00Fail
related talks
20mKanren Light
19mSome Novel miniKanren Synthesis Tasks
17mλKanren: Higher-order Logic Programming with Shallow Embedding
26mtypedKanren: Statically Typed Relational Programming with Exhaustive Matching in(…)
40mμKanren: Running the Little Things Backwards
22mA Case Study in Functional Conversion and Mode Inference in miniKanren
47mLogic Programming à la Carte
15mAn Empirical Study of Partial Deduction for miniKanren