7ML7W Minikanren Days 1 3
It's like kanren, but smaller.
We introduce ourselves in what we'll charitably call some sort of order, and then we're off. A rubric is rubred.
There's a lot in here, and we're not completely sure it's a single meeting - let's do one and see where we get.
Mooted that we could maybe have a play with core.logic based on the chapter as the first meeting, but then perhaps explore how it actually works (which the book doesn't cover at all) as an optional second meeting, if we feel like it.
Mudge: let's implement microkanren in php
All: [awkward silence]
[brief interlude while Murray installs Java]
Elena: Anyone want to know what "kanren" means?
All: hell yeah
Elena: it means "relation" in Japanese
[ooohs]
Mudge: What is a relation anyway?
Tom: It's basically a list of tuples. Functions are a special case of relations where for each input there's only one output. But the general case there could be multiple "outputs" for a given input. Think of "less-than" vs "double" - with the latter, for any given number there's only one number that's double it. Whereas for any given A there's infinitely many Bs that it is less-than.
So is core.logic the same thing as minikanren? We're not completely sure. The book says it's a clojure implementation of minikanren, but there isn't really a good reference we've been able to find that says what minikanren really is. Nor does the book really explain the connection much. Maybe it's assumed based on the previous book having a Clojure chapter?
The naming "core.logic" doesn't imply much - "core" in this context just means it's part of the clojure stdlib, we think.
Murray: We get this warning about overriding == - doesn't that make this hard to use?
Mudge: in practice you'd keep it namespaced, so you'd use something like (logic/== q 1) or maybe a terser alias.
Mudge: What's this _0 you get when q (say) doesn't have a value?
It means the variable is unbound - the numeral is a global identifier, so newly-introduced variables will have different identifiers.
There's some chat about unification - what is it, and why has it replaced "regular" equality?
Well, it's essentially bi-directional matching. We take two sides of the equality and bind them to values that make both sides equal (if that's possible).
Simon: There's different kinds of equality in logic programming - we can test for "identically equal" and possibly other things, but unification is kinda the core equality concept in logic programming.
[we play around with membero - querying it "forwards" and "backwards"]
Q: What does it exactly mean by "backwards"? It's not brilliantly motivated.
Murray: I guess if you think in a regular language, you can imagine writing a function that tests if an element is in a list, but it's hard to imagine the same code also giving you all the lists that element is a member of, and that's what this is doing. One definition, multiple ways of querying it.
Murray: What's with this -o then? We don't really know why it's that, but at least it helps denote relations; it's nice to know what kind of thing you're dealing with.
Rumours abound that it's supposed to look like the "top of a question mark", particularly if you have a superscript "o". Presumably this was decided by someone who'd had question marks described to them once, but had not actually seen one.
Tom: That's worse than no explanation. (╯°□°）╯︵ ┻━┻
We chat a bit about embedded languages, and the benefits of being able to hop out of core.logic into clojure's functional and lazy stream processing stuff.
James C: There's also a risk here; I found when implementing microkanren in ruby it's really easy to mix the different concepts, and find yourself implementing something using the host language's primitives when you should be using the guest language's concepts instead.
- 77% OF DOGS SUPPORT BREXIT
- NIGEL MANSELL'S MOUSTACHE IS INSURED FOR SEVEN POUNDS FIFTY AND A SMALL QUANTITY OF PEAS
Oh also there's this logic.pldb thing, which lets us define databases of facts.
Simon: There's a maybe little bit of a divide between these facts and relation definitions, whereas in Prolog the only difference between a fact and a rule is that facts are fully-instantiated, and don't have a definition body?
Still, once you're within a (with-db ...) clause you can query facts like any other relation.
Tom: [re the vitalo relation] I was disappointed that this definition of alive computer scientists hasn't become outdated since the book was published.
Ruling out the possibility of Alonzo Church rising from the grave to wreak bloody havoc on the natural numbers (again), we have to assume that the still-alive computer scientists are pretty content with this state of affairs, however.
Anyway. We see a fact db, and observe that it can be queried. Jolly good.
Tom: What does [] mean in clojure? It's a vec right? Why do we use this in particular for arg lists?
Murray: (run (q) (== q 1)) => (1) apparently NO REASON AT ALL.
[something to do with quoting wot I missed]
We chat about goal ordering - does it matter? Conceptually no - it can make a difference to performance, however (because the goals are executed in some order). With different instantiation patterns (e.g. running a relation "forwards" or "backwards"), it can affect whether you get results or enter an infinite loop.
Later we'll see things that modify the search tree as goals succeed (e.g. conda, condu), but these are kinda "non-relational" things (it'll say this in the docs for them), so it's sort of a new layer of things to think about.
We look at conde and check out getting multiple answers. What does (run 1 [q] & goals) return? The first result is basically implementation-dependent - it's whatever the underlying execution scheme happens to succeed at first.
Mudge: it's interesting that conso has more arguments than we'd expect - 3 vs 2.
Murray: Yeah, cos we also need to represent the "result" - there's no "return value" for relations, we're describing the relationship between three things.
In fact there's no fixed "result" argument since you can run it backwards - what's "input" and "output" depends on the instantiation pattern of the arguments you query it with.
We're reimplementing membero like the cool kids.
(defn insideo [e l]
(conde
[(fresh [h t]
(conso h t l)
(== h e))]
[(fresh [h t]
(conso h t l)
(insideo h t))]))Tom: why are there multiple fresh calls in here? Can we lift that up above the conde call?
[furious Murray-typing]
(defn insideo [e l]
(fresh [h t]
(conde
[(conso h t l) (== h e))]
[(conso h t l) (insideo h t)]))This works. We're not sure if the difference is important.
Murray: I wonder if it's because now they introduce matche, and the first form is what matche would expand to?
Okay, so we look at matche.
(defn insideo [e l]
(matche [l]
([[e . _]])
([[_ . t]] (insideo e t))))Murray: We have to match against the whole argument array - in this case there's only one, but that's what gives us these ugly [[]] around each match expression.
Tuzz: So is this restricting the search space? If the first match succeeds, will it carry on trying the second clause?
Yep - this conde is the unrestricted form. There's no constraint on the second clause either, so even if it finds e once, it'll keep looking in the rest of the list if you ask it to.
defne then - a matche time-saver:
(defne insideo [e l]
([[e . _]])
([[_ . t]] (insideo e t)))We decide to have a go at the Day 2 exercises. These have a dependency on the the Day 1 exercises, so we first try to write extendo/3, which is a reimplementation of appendo/3
[INSERT CODE HERE]
Okay, we got a bit into the weeds here. We tried to do a straight conde version (no matche, no defne), and after a few false starts actually doing the recursive definition, arrive at:
(defn extendo [a b l]
(conde
[(== a [])
(== b l)]
[(fresh [h t t2]
(conso h t a)
(extendo t b t2)
(conso h t2 l)])))This doesn't work with querying (run* [q] (extendo q [3 4] [1 2 3 4])) - it heads into an infinite loop.
Via some looking at a defne solution we realise we can reorder the conso calls:
(defn extendo [a b l]
(conde
[(== a [])
(== b l)]
[(fresh [h t t2]
(conso h t a)
(conso h t2 l)
(extendo t b t2)])))While we naturally wrote it last because it feels like the final "step" of the solution, in fact the constraint it applies is vital to constrain the recursive case and stop it looping infinitely.
-
We took a somewhat more superficial approach to this language, unlike some of the others. That might be fine, but was it ideal as a meeting format? Did people who hadn't got through all of the chapter follow along?
-
Do we want another meeting on this? Mudge would like to have more of a play, perhaps solve a problem we otherwise couldn't have.
Murray: it's the "running it backwards" for me, getting different variations of the problem for free. Could we write a simultaneous sudoku solver + generator?
- Mobbing an implementation of some... thing (waves hands) could work as a meeting?
There's not much dissent, so let's have a chat on slack about mob programming "a thing" in minikanren.
Organiser: Simon C volunteers, pretty heroically though he says so himself. It'll be on the 4th. Or it might not cos Simon's not here. A doodle will ensue.