Re: [Chicken-users] New Egg: miniKanren

[Jeremy Steward]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Note to the mailing list: apologies for the really long email ahead.
If this is too long please let me know and I won't do it again. I also
assume some knowledge of the Reasoned Schemer / miniKanren for my
response below, so if you do not know either then the following
descriptions may be sparse.

Hi Alex,

On 17/02/16 01:03 AM, Alex Silva wrote:
| Sorry for veering off-topic, but: As someone who has read the
| Reasoned Schemer, how would I go about learning this improved
| language?

No worries, I was also confused at first that the language had changed
as much as it had. All things considered these aren't "large" changes
but the style of code you write becomes very different on it's own as
well. If you want a deep explanation of how things work internally, I
can only suggest William Byrd's dissertation:

Original: http://gradworks.umi.com/33/80/3380156.html
Single-spaced: https://github.com/webyrd/dissertation-single-spaced

Nonetheless, to adapt to the latest version of miniKanren, you only
need to consider what I mentioned above in list form, since otherwise
pretty much all semantics are the same. I'll try to break it down and
go through it, if the mailing list will forgive me.

| 1. condi no longer exists 2. conde now behaves like condi

Basically, you just need to retrain yourself to think of using conde
wherever you would use condi before. The main difference between these
was more or less "how you search": whether you performed a depth first
search along a single branch (old conde) or depth first search
interleaved between branches (condi).

Here's an example from The Reasoned Schemer that should (hopefully)
illustrate what's gone on here:

OLD MINIKANREN
==============

~    (run 5 (q)
~      (conde
~        ((== #f q) alwayso)
~        ((== #t q) alwayso)
~        (else fail))
~      (== #t q))

This runs forever, because the first conde line succeeds, but the
outer (== #t q) fails. Since alwayso will succeed an infinite number
of times, conde will try again, the first line will succeed, the outer
(== #t q) will fail, and so on and so on.

Instead, they introduce condi, which doesn't test the same branch in
order every time:

~    (run 5 (q)
~      (condi
~        ((== #f q) alwayso)
~        ((== #t q) alwayso)
~        (else fail))
~      (== #t q))

Here condi will still fail on the first branch, but instead of trying
the first branch again from scratch, will instead switch to the second
branch. This will succeed, which gives you a result. This behaviour in
general means that if an answer logically exists, miniKanren will find
it and return it eventually. This means it has better termination
guarantees, since the original conde just searches down the first
branch forever. Instead consider the latest miniKanren

LATEST MINIKANREN
=================

~    (run 5 (q)
~      (conde
~        ((== #f q) alwayso)
~        ((== #t q) alwayso))
~      (== #t q))

The extraneous else statement is removed, more on that below. However,
this runs exactly like the condi version above. My understanding is
that William Byrd found the stronger termination guarantees more
useful in practice than the Prolog-like behaviour of searching a
single branch again and again and again.

**NOTE** As an aside, since condi is gone, so are all, alli, etc that
were present in The Reasoned Schemer, as they are also no longer
needed (their primary use was to implement condi, IIRC).

| 3. else is removed as syntax from conde, conda, and condu

At first this one bothered me too, but I sort of warmed up to it. It
means you can't have an (else expr ...) branch in a conde, conda, or
condu expression. This makes it a little different from Scheme's cond,
however consider that "else" doesn't make much semantic sense in the
context of logic/relational programming anyways. I mean, you're just
performing a search down a set of branches in a conde expression, and
unlike cond, the else branch of a conde expression doesn't mean that
every other branch failed (this is implicit in cond, but in conde
you'll find that may not be true).

So instead of writing else branches, just write the expressions as you
would normally for any other branch. As an example, consider the
following (note I'm going to try and assume no other procedures are
defined other than unification).

Instead of:

~    (define (appendo l s out)
~      (conde
~        ((== '() l) (== s out))
~        (else
~          (fresh (a d res)
~            (== `(,a . ,d) l)
~            (== `(,a . ,res) out)
~            (appendo d s res)))))

You could just write:

~    (define (appendo l s out)
~      (conde
~        ((== '() l) (== s out))
~        ((fresh (a d res)
~           (== `(,a . ,d) l)
~           (== `(,a . ,res) out)
~           (appendo d s res)))))

Even in the old miniKanren, both of these would have worked the same.
Adding "else" as syntax is kind of redundant and makes for visual
noise. This is made somewhat worse by the fact that (else fail) is
used heavily in the book, which makes no sense. If no branch succeeds,
failure is implicit, so (else fail) can be pretty much removed for
this reason in all instances.

| 4. the latest version introduces disequality constraints (=/=) as
well as some type-constraint operators (absento, numero, symbolo,
booleano).

These are the most interesting change, because they allow you to do
some neat things that weren't possible using miniKanren from The
Reasoned Schemer. William Byrd has an entire chapter dedicated to =/=
in his dissertation, which is pretty brilliant in it's own right.
Using the constraint operators, there's even implementations of
relational interpreters built on miniKanren
(https://github.com/webyrd/quines).

Nonetheless, how to use these is pretty simple, but I'll just stick to
=/= for now since it's probably the most useful. The easiest way to
get to know it is to play with it, so here's the simplest example:

~    (run 1 (q) (=/= q 5))  ;=> ((_.0 (=/= ((_.0 5)))))

This tells us q can be anything, as long as it's not 5. On it's own,
not very useful; however this turns out to be useful for rembero,
defined in The Reasoned Schemer, which normally looks like this:

~    (define (caro l a)
~      (fresh (d)
~        (== `(,a . ,d) l)))

~    (define (rembero x l out)
~      (conde
~        ((== '() l) (== '() out))
~        ((caro l x) (cdro l out)) ; The car of l is equal to x, or unify
~        ((fresh (a d res)
~           (== `(,a . ,d) l)
~           (== `(,a . ,res) out)
~           (rembero x d res)))))

This is the definition (slightly modified) that is given in the book.
However, if you run it:

~    (run 3 (q) (rembero 5 '(5 5 3 4 5) q))

~    ;=> ((5 3 4 5) (5 3 4 5) (5 5 3 4))

Which is incorrect, because rembero should act like rember, which only
removes the first instance of the atom 5 from the list '(5 5 3 4 5).
The only answer here should be the first one (every other 5 removed
would be an error).

So the fix is easy, tell rembero that before it can recurse, x cannot
be equal to a. Since we only want to enter the last branch if the
first and second branch fail, then we need to be explicit about this.
Thus, the proper way to implement rembero:

~    (define (rembero x l out)
~      (conde
~        ((== '() l) (== '() out))
~        ((caro l x) (cdro l out)) ; The car of l is equal to x, or unify
~        ((fresh (a d res)
~           (== `(,a . ,d) l)
~           (=/= a x)              ; The car of l is not equal to x
~           (== `(,a . ,res) out)
~           (rembero x d res)))))

To be more explicit we could also throw (=/= '() l) above our fresh
clause but (== `(,a . ,d) l) does this already. Now our example:

~    (run 3 (q) (rembero 5 '(5 5 3 4 5) q))

~    ;=> ((5 3 4 5))

Only one answer appears. You really need to play with these features
to grasp how to use them best. The idea of using disequality to be
explicit about branch selection is weird, especially since it doesn't
match similar behaviour to cond, but that's just a part of relational
programming. I apologize for the long mail, but hopefully this
summarizes the majority of the changes between the languages.

William Byrd even discusses some of this history throughout the
following two videos from 2014:

https://www.youtube.com/watch?v=zHov3fKYqBA (part 1)
https://www.youtube.com/watch?v=nFE2E91VDAk (part 2)

Unfortunately they are quite long and I don't have timestamps for any
specific references or quotes. They're fun to work through though, as
part 2 he actually goes into detail into how to build a relational
interpreter.

Hopefully that clears things up, sorry to the mailing list if this is
too long and too wordy. I only looked at the length after writing it,
and probably could have turned this into a blog post of it's own.

Regards,

- -- 
Jeremy Steward

-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2

iQIcBAEBAgAGBQJWyMcfAAoJEHVwwAZUeZnZgOQP/RteL1dof6bgaCFf6Ytdwz9z
P8/UfdR/7/3U3MqPydnq3YTnz/qOCgPSwNF39NlxFu6Ndcs2IvCPP6AR94ZJ5p4b
eMaH9juF0O5u1IbA4N3I7xmbNLzsnC1h8UuMdpafSEUMki2F9rsJ6uFFepZi3Dc4
vf5AueLhaTlFZ+6/81CZ0z50awQPQjKnXweqT7xJv4c7kI18GxEyusDRE22iokyd
t9K537ohRgUsgfrvK854Lg1KWgotVgLUQBn4YMDkSu3pzWVmUE6tLPPOw5KYz723
mDIzVvdIJzXsdtwP4yMQ8rUBISV8nQKlJNZen7VpDty3FJJ/jeiNhHWTEkMMOkvT
XW6atH2FVxqtaHCbf5DarKRY6ciTs0l4VjqWVc5Mb+wdu7TvvB4rkmN/YInLLe0w
Sd5TgsZf1/VKPlSWi6Lcr/wePHJOcVqIPmUYlJE0zw5LOL/m6VCxikv0H6qm5a8x
Ej3djbVgQxnSbd6BYjevZw4VArYFziu9chdCg01jceBrBOyfOfhZEICyYFpNeHJE
Rv78Tj4w3t8FAxhZ4v8zL+kh7R0Nkh9odw2n3KN2QQHlSlg+IukJG1VlLsMjzpXl
ucXFUv7tA976neF7fgU2g9mO4BLxVMFD9/XIjfWcnvPxZKO3mePddSStxosOpM/n
nK638k4tyyjppRPUu0Wm
=BjxG
-----END PGP SIGNATURE-----