An implementation of miniKanren in Haskell
clone the repository and open examples.hs like so:
ghci -isrc examples.hs
If you want to make it work with your own type you can basically just replicate what's in Control.Monad.MiniKanrenT.Term replacing Term with your own type.
As far as I know the semantics are essantially the same except:
- Logic variables are typed (and you can define your own custom types)
- conde is actually condi and it doesn't have an else clause (as it doesn't do anything special anyway)
- My implementation will not go into an infinite loop if a unification is circular. There is no "occurs check" and it doesn't need one.
This year at strangeloop 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.
They 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.
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 :)