-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
