I would look at uKanren, the smallest mini-kanren cousin. I like Bodil Stokke's [1] introduction, but if you are not afraid of lisp, you can read/re-implement t

I would look at uKanren, the smallest mini-kanren cousin. I like Bodil Stokke's [1] introduction, but if you are not afraid of lisp, you can read/re-implement the original(?) [2] paper :) It is basically bunch of combinators for depth-first search? So if you think "I kinda want to brute-force solution for these hard-coded constraints", you might instead want to create a simple logic-programming environment first :-) Last time I played with these, I used it for implementing a toy cryptograhic protocol verification system for a term project. It have barely worked :D A.f.a.i.k. type-checkers often use some sort of logic programming at their core. [1] https://paperswelove.org/2015/video/bodil-stokke-%CE%BCkanren/ https://paperswelove.org/2015/video/bodil-stokke-%CE%BCkanre... [2] http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf