Hi, Racket Discourse.
I am busy researching μKanren to see if it would be suited to some tasks at work, and I thought to share some of my observations on the subject.
So, the papers I am reading, are:
- µKanren: A Minimal Functional Core for Relational Programming
- A Framework for Extending μKanren with Constraints
The second paper in particular, is quite interesting. It describes a driver for creating encapsulated constraint systems, building off of an "axiomatic" implementation of == (the unification goal).
Basically, each constraint operator is given its own substitution context, which is then recruited to invalidate any new unifications as one tries to solve a given goal.
The text is very easy to follow, although I am curious about how the invalidation rules were generated for the various constraint operators.
Specifically, there is a bit in the text for defining not-pairo which looks like:
(λ (s)
(ormap (λ (n)
(let ((t (walk n s)))
(not (or (not (pair? t)) (var? t)))))
not-pairo))
where s is the current == substitution context, and n is an element of the substitution context for not-pairo.
This stands out, because of the boolean expression, (not (or (not (pair? t)) (var? t))).
Applying De Morgan's law, we see that it is simply:
(not (or (not (pair? t)) (var? t)))
-> (and (pair? t) (not (var? t)))
; if it isn't a pair, it will fail, irrespective of the second term
-> (pair? t)
Not really a big deal, but I have been scratching my head about why this would be phrased this way, given that it seems to simplify handily. Am I missing something?
I opted to diverge from the paper's implementation somewhat, for fun, by not using natural numbers, nor vectors of a single natural number to represent variables, but instead using opaque structs with no fields.
This made some things easier, but when it came to reifying the results from a particular query, I was left perplexed, because the implementation they provide in the second paper does not impose any particular ordering on the variable and non-variable terms in the pairs which make up the bindings of a substitution context. They are simply recorded as is.
For example, the "raw" result of the following query:
(define-syntax-rule
(run* (x ...) g₀ g ...)
(let ([x (var)] ...)
;; I use § to mean system (S in the paper)
(define §* (take-all (call/empty-state (conj* g₀ g ...))))
(for/list ([§ (in-stream §*)])
(hash-ref § '≡))))
(define (append-o l s r)
(cond-o ;; I just use `-o` for everything, but this is technically `cond-e`
[(≡ null l) (≡ s r)]
[(fresh (a d r′)
(≡ (cons a d) l)
(≡ (cons a r′) r)
(append-o d s r′))]))
(pretty-print
(run* (q)
(append-o '(a b c) '(d e) q)))
'((((d e) . #<var>)
(() . #<var>)
((#<var> . #<var>) . #<var>)
((#<var> . #<var>) . #<var>)
((#<var> . #<var>) . #<var>)
((#<var> . #<var>) . #<var>)
((#<var> . #<var>) . #<var>)
((#<var> . #<var>) a b c)))
As you can see, the valid substitutions may appear in any order, and are not normalized by default.
Now, because I do not use natural numbers to indicate the ordering of the variables, from least to most recent, I could not employ the method of projection the paper defines.
However, if one thinks about this for a bit, you realize that each of these pairs are in fact unifiable!
That is to say, to impose a projection over them, you can simply unify the pairs, and then do the reification as per normal.
Fortunately, the paper already defines a procedure for doing just this, called valid-==:
(define (valid-== ==)
(foldr (λ (pr s) (and s (unify (car pr) (cdr pr) s))) '() ==))
where == is the substitution context for unification, and each pr is an element thereof.
Thus, we can define a projection π which gets everything back into shape:
(define (reify u ¢)
(let ([v (walk u ¢)])
(cond
[(var? v) v]
[(pair? v)
(cons (reify (car v) ¢)
(reify (cdr v) ¢))]
[else v])))
(define (project §)
(let ([¢ (valid≡ (hash-ref § '≡))]) ;; I use ≡ to mean ==,
;; and ¢ to mean substitution context
(lambda (x) (reify x ¢))))
(define-syntax-rule
(run* (x ...) g₀ g ...)
(let ([x (var)] ...)
(define §* (take-all (call/empty-state (conj* g₀ g ...))))
(for/list ([§ (in-stream §*)])
(let ([π (project §)])
(list (π x) ...)))))
Now, everything makes sense.
(for-each
displayln
(run* (q)
(append-o '(a b c) '(d e) q)))
'((a b c d e))
I haven't thought about whether this could be streamlined earlier in the process, but I thought it was neat that the total number of modifications to the paper's outline was minimal to support the use of non-indexed variables.
Mooiloop.
My implementation isn't great, but if you'd like to take a gander: