miniKanren in Haskell

This year at Strange Loop I was totally blown away by the miniKanren talk by Daniel Friedman and William Byrd. I highly recommend watching the presentation. It is simultaneously entertaining and mind blowing.

Friedman and Byrd used an extended version of miniKanren, a logic programming language (a la prolog) embedded in scheme, to do several remarkable things:

• Generate programs that evaluate to a given value,
• generate programs that satisfy a given type,
• and (most awesomely) generate Quines! — and Twines!!

This was something that I clearly did not know enough about yet. Usually when I want to really learn and understand something in CS, I try to implement it. So I grabbed a copy of The Reasoned Schemer and did just that!

My weapon of choice is Haskell, so here you go, a miniKanren monad transformer in Haskell: miniKanrenT.

Monad Transformers FTW!

It turns out there is a very nice monad transformer by Dan Doel (based on a paper co-authored by Friedman) that does the backtracking and interleaving for me. I’ll still likely have to take a shot at making my own version of logict (again, just to learn how it works), but this will work for now.

However, I couldn’t find a suitable Haskell logic variable implementation, so I made one that can be safely used in a monad transformer. That means it will work correctly even with the backtracking and branching that the logic monad does. And it also means that I can basically plug the two monads together to make a miniKanren monad!

This is not quite the MiniKanren in the talk. They have “does not unify” operator =/= that I don’t have implemented… yet. But I think it does correctly implement the core features of miniKanren as described in The Reasoned Schemer.

I’m not quite satisfied with implementation yet. I still want to implement the remaining features necessary to be able to generate my own quines. :) I also want to implement some of the “libraries” for working with numbers and lists and such.

So there should be more to come.