This is the second part of my bookshelf, a series of posts about a couple of books I'm reading.
Unlike the CouchDB book, The Reasoned Schemer(TRS henceforth) is a book that you don't simply read on the couch, but actually study. This is why it took weeks rather than days to come to this point, where I understand how to use(but not implement) miniKanren.
The book has a gradient on the cover, which gives it the impression of a technical book(it's from MIT press), but it actually contains drawings and the typesetting is brilliant(it is written with some sort of LaTeX I believe). It is also very suitable for vegetarians, since it uses vegetarian food rather than foo/bar/baz.
The book is written in questions and answers, both in separate columns. You could overlay the answers, and try them yourself first.
TRS describes miniKanren, a logic programming language. It is the bare essence of Prolog and Kanren, written in a few hundred lines of Scheme.
I used
Logos, an implementation in Clojure by David Nolen, to follow the examples in the book. This worked out very well, but there are a couple of minor differences.
- fresh is called exist in Logos.
- Logos uses vectors for binding variables.
- Everything is interleaving, so there are no cond-i and all-i.
- Clojure does hot have pairs, and only proper conses are allowed, it uses lcons instead.
- Clojure has first and rest, so car-o and cdr-o are called after their clojure.core counterparts.
Later in the book, an arithmetic system is implemented in miniKanren. I attempted to
port it to Logos, though it is not complete and bug free yet.
I do not yet fully understand the last few chapters of the book, one of which describes unification. The last chapter is unique in the book in that it does not use the question-answer style, but rather explains the inner workings of miniKanren in tightly packed chunks of information.
I really enjoyed the book, and I hope to find some good uses for my newly acquired powers.
