From Prolog to Hindley Milner
In this talk, I introduced logic programming with Prolog, went over how to implement unification in Haskell and talked about how type inference and typeclasses can be thought of in terms of logic programming.
Here's the code for the whole unification function; you can probably remember each individual part from the talk.
unify :: Predicate -> Predicate -> Maybe MGU unify (Predicate _ name1 body1) (Predicate _ name2 body2) | name1 /= name2 || length body1 /= length body2 = Nothing | otherwise = foldM combine  $ zip body1 body2 where combine mgu (left, right) = go mgu (subst mgu left) (subst mgu right) go mgu (Var l) r | not (r `contains` Var l) = Just $ (l, r) : mgu go mgu l (Var r) | not (l `contains` Var r) = Just $ (r, l) : mgu go mgu (Pred l) (Pred r) = merge <$> unify l r <*> Just mgu go mgu l r = if l == r then Just mgu else Nothing
The only line I didn't actually cover is what
combine. This is actually just a little helper function that takes the two terms I'm unifying, updates them with the MGU so far and calls the actual case-by-case part of the unification algorithm on the results.
You can see the entire code (although without comments) on GitHub. I also included a few demo prolog (.pl) files you can play with, either by running my interpreter or using a real one like swipl. These files contain most of the Prolog code from my talk and some comments to help explain what's going on and give you a few exercises to better understand logic programming.
Right now, the slides themselves are a little broken, so I'm not putting them up yet.
I've also been thinking about doing this talk again, maybe at one of the Haskell meetups. So if you're interested but missed it—or, for whatever reason, want to see it again :)—you'll probably have a chance. I'll also try to improve it based on feedback I've gotten; if you have anything to say, please email me at email@example.com. (I especially appreciate criticism and hearing about what you found confusing or poorly explained!)