https://github.com/ashton314/muKanren_reading Skip to content Sign up * Product + Features + Mobile + Actions + Codespaces + Packages + Security + Code review + Issues + Integrations + GitHub Sponsors + Customer stories * Team * Enterprise * Explore + Explore GitHub + Learn and contribute + Topics + Collections + Trending + Learning Lab + Open source guides + Connect with others + The ReadME Project + Events + Community forum + GitHub Education + GitHub Stars program * Marketplace * Pricing + Plans + Compare plans + Contact Sales + Education [ ] * # In this repository All GitHub | Jump to | * No suggested jump to results * # In this repository All GitHub | Jump to | * # In this user All GitHub | Jump to | * # In this repository All GitHub | Jump to | Sign in Sign up {{ message }} ashton314 / muKanren_reading Public * Notifications * Fork 0 * Star 19 A close reading of the mKanren paper. 19 stars 0 forks Star Notifications * Code * Issues 1 * Pull requests 0 * Actions * Projects 0 * Wiki * Security * Insights More * Code * Issues * Pull requests * Actions * Projects * Wiki * Security * Insights This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository. master Switch branches/tags [ ] Branches Tags Could not load branches Nothing to show {{ refName }} default View all branches Could not load tags Nothing to show {{ refName }} default View all tags 1 branch 2 tags Code Latest commit @ashton314 ashton314 Add example of program synthesis ... 4d41f61 May 25, 2022 Add example of program synthesis 4d41f61 Git stats * 10 commits Files Permalink Failed to load latest commit information. Type Name Latest commit message Commit time README.org Add example of program synthesis May 25, 2022 kanren.rkt Add example of program synthesis May 25, 2022 relations_playground.rkt Add predicate checking May 22, 2022 type_checking.rkt Add type checker, applications section May 25, 2022 View code [ ] Notes on mKanren Synopsis Description Implementing the Core Basic types The walk function Implementing unify Implementing call/fresh AND and OR goal constructors What are streams? Extensions Modifications Variable representation Predicates in unify Applications Family tree relationships Type checking Author Further reading Footnotes README.org Notes on mKanren Synopsis I wanted to understand how mKanren works. This is an annotated journey through implementing the code from that paper. Description mKanren is a very small implementation in the Kanren family: essentially these are little embedded Prolog implementations. mKanren is particularly interesting because its implementation is less than 40 lines of Scheme code, and makes no use of exotic language features. Indeed, if your language has closures, you can make yourself a mKanren. Implementing the Core Basic types state :: subst x fresh_var_counter subst :: assoc list mapping variable - variable | value goal :: state - state* Goals take a state and return a stream (lazy) of zero or more new states. A state tells us a variable substitution that satisfies the constrains the goals created. The walk function This takes a variable and a substitution list, and it will walk through the substitution list until it finds the ultimate reference of the variable given. Since variables can map to other variables in the substitution list (see the Basic types section) then walk traverses those transitive dependencies until it can't any more. It can return another variable; if the last thing that one variable points to is another variable that is not present at the beginning of the list, then returning that variable is valid. This is important for the unify function. Implementing unify The unify function take two things, u and v, and tries to make them line up according to the substitution that you give as well. (unify '(1 2 3) '(2 3 4) '()) #f (unify '(1 2 3) '(1 2 3) '()) '() (unify '(1 2 3) '(1 2 3) '(yay)) '(yay) (unify (list 1 2 3) (list 1 (var 0) 3) '()) (list (cons (var 0) 2)) (unify (list 1 2 3) (list 1 (var 0) 3) `((,(var 0) 4))) #f This example illustrates how the walk function drills down: (walk (var 0) `((,(var 0) . ,(var 1)) (,(var 1) . ,(var 2)))) (var 2) (unify (list 1 2 3) (list 1 (var 0) 3) `((,(var 0) . ,(var 1)) (,(var 1) . 2))) (list (cons (var 0) (var 1)) (cons (var 1) 2)) If we wanted to be able to unify more than just lists (e.g. rich structures) we would teach mKanren here in the cond how to walk those richer structures. Successful unification returns the substitution list that made the two things unify. This is different from the passed-in substitution list when a variable is found to point to another variable. Implementing call/fresh The implementation of call/fresh depends on the structure of the state: in a pure language, we stick a fresh variable counter on the state so we can thread that fresh effect through the computation. I would like to try just using something like gensym for variable creation. AND and OR goal constructors The magic of the disj and conj functions is encapsulated in the mplus and bind functions. With the disj function, we want to OR two goals, and the conj is to AND two goals. For disj, we run both goals and add them together. For conj, we run the first goal (seen by applying the first goal to the subst/counter variable) and then we thread the result of that to the second goal. Exactly how we add the goal results together bzw. thread the state from one goal to another determines the properties of the search. I'll skip the detailed evolution of this (see the paper for a nice walk-through) but in the end we get lazily-evaluated interleaving stream handling so we can exhaust every finite stream. What are streams? Streams are lists of states with lazily-evaluated members. Here's an example from the paper showing how streams need to be interleaved and be lazy: (define (fives x) (disj (== x 5) (l (s/c) (l () ((fives x) s/c))))) (define (sixes x) (disj (== x 6) (l (s/c) (l () ((sixes x) s/c))))) (define fives-and-sixes (call/fresh (l (x) (disj (fives x) (sixes x))))) Extensions These are some syntactic sugar that make working with mKanren nicer. Most of them are macros, which would make porting these to other languages less straight-forward. But they do make working in Scheme/ Racket a lot nicer. Some new non-Lisp languages like Elixir[fn:1] feature hygienic macro systems, so these features would be portable. Modifications Variable representation I deviated from the paper's implementation of variables and wrote them as structs instead of vectors. I think further changes could be made (e.g. not having to keep around a number in the state to generate fresh variable names but these might rely on some more language-specific features. (E.g. generating fresh strings/symbols.) Predicates in unify I've added some rudimentary predicate checking to the unify function: (define (fav-num n) (disj (== n 42) (== (cons '? even?) n))) > (run* (n) (== n 12) (fav-num n)) '(12) > (run* (n) (== n 13) (fav-num n)) '() > (run* (n) (fav-num n)) '(42 (? . #)) Applications Family tree relationships The classic example. See ./relations_playground.rkt. Because of how the relations are defined, this will print out an infinite list of relations if you try to run certain queries, so best use the run function with some finite (and preferably small number; it doesn't take much to cover the whole space at least once) bound, as opposed to just running run*. Type checking See ./type_checking.rkt for an implementation of a simple type checker/inference algorithm. Here is how you check the type of a program: > (run* (type) (type-for '((lambda x x) 2) '() type)) '(number) > (run* (type) (type-for '((lambda x (zero? x)) 2) '() type)) '(boolean) > (run* (type) (type-for '((lambda x (zero? x)) #f) '() type)) '() ;; type error > (run* (type) (type-for '(lambda x x) '() type)) '((_.5 . _.5)) ;; generic type: a -> a Here's the crazy thing: you can actually ask for programs that match a given type, since relations work both ways. Here's an example of generating five programs that are of type number - boolean: > (run 5 (prog) (type-for prog '() (cons 'number 'boolean))) '((lambda _.1 (? . #)) (lambda _.1 (zero? (? . #))) (lambda (? . #) (zero? (? . #))) (lambda _.1 (zero? (+ (? . #) (? . #)))) (lambda _.1 (if (? . #) (? . #) (? . #)))) Author I hope is very clear that I did not write the mKanren paper. That would be Daniel P. Friedman and Jason Hemann. I merely wrote up this annotation. Ashton Wiersdorf Further reading Be sure to read the actual paper which is freely available. Other fun links: * Unifying the Technical Interview Footnotes [fn:1] Personally, I think of Elixir as a Lisp in Ruby's clothing running on the BEAM. But don't tell anyone that Lisp is quietly becoming the new hot thing in web development and some machine learning. About A close reading of the mKanren paper. Resources Readme Stars 19 stars Watchers 1 watching Forks 0 forks Releases 2 tags Packages 0 No packages published Languages * Racket 100.0% * (c) 2022 GitHub, Inc. * Terms * Privacy * Security * Status * Docs * Contact GitHub * Pricing * API * Training * Blog * About You can't perform that action at this time. You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.