I am reading minirop.pdf and it seems to be written in a dialect of MiniKanren that is outdated. I am interested in how I can port this style of MiniKanren to miniKanren-with-symbolic-constraints, since that seems to be more widely used.
I have to make a couple of adjustments, like replacing exists
, but the code seems to work with the current version of the CVS repo on https://kanren.sf.net.
For example, all
, which is used in common-ancestor
:
~/kanren/mini $ scheme type-inference.scm
Chez Scheme Version 9.5.8
Copyright 1984-2022 Cisco Systems, Inc.
[... bunch of omitted test output ...]
> (define father
(lambda (dad child)
(conde
((== dad 'jon) (== child 'sam))
((== dad 'jon) (== child 'hal))
((== dad 'sam) (== child 'rob))
((== dad 'sam) (== child 'jay))
((== dad 'sam) (== child 'roz))
((== dad 'hal) (== child 'ted))
((== dad 'rob) (== child 'sal))
((== dad 'rob) (== child 'pat)))))
> (define child
(lambda (child dad)
(father dad child)))
> (define ancestor
(lambda (anc desc)
(conde
(succeed (child desc anc))
(succeed (fresh (paren)
(child desc paren)
(ancestor anc paren))))))
> (define common-ancestor
(lambda (anc desc1 desc2)
(all
(ancestor anc desc1)
(ancestor anc desc2)
(project (desc1 desc2) (if (not (eqv? desc1 desc2)) succeed fail)))))
> (run 2 (a) (common-ancestor a 'sal 'jay)))
(sam jon)
This is the expected result. However, all
isn't available in with-symbolic-constraints. Intuitively, I don't even understand why it should be necessary, since The Reasoned Schemer (2nd ed.) doesn't use it, it just puts consecutive conditions after each other. So I was thinking I could just remove it, and it should work in with-symbolic-constraints. But as you can see, that doesn't work:
~/with-symbolic-constraints $ scheme mk.scm
[... required definitions omitted, they are the same as above ...]
(define common-ancestor
(lambda (anc desc1 desc2)
(ancestor anc desc1)
(ancestor anc desc2)
(project (desc1 desc2) (if (not (eqv? desc1 desc2)) succeed fail))))
> (run 2 (a) (common-ancestor a 'sal 'jay)))
(_.0)
How do I write common-ancestor
nowadays? Is the problem with all
or is it with the projection?
The expression
((lambda ()
a
b
c))
will always return c
, whatever a
and b
are (unless they do some non-local control flow such as using continuations). So unless a
and b
have side effects, you might as well have just written c
instead of the whole lambda invocation. In particular, if a
and b
are goals, they are ignored, and your lambda just produces the goal c
anyway.
You need something to combine them into one compound goal, and all
is a traditional name for a combinator that does this. But in the absence of all
, observe that fresh
does the same thing: all the goals under a fresh
are combined. So you can just use (fresh () ...)
as a substitute for (all ...)
, or indeed define all
yourself as a function (or macro) that takes multiple goals and combines them with (fresh ())
.