guile-minikanren-uncourse-code/appendo.scm

;; import miniKanren
(use-modules (faster-miniKanren mk-guile))

;; normal append function
(append '(1 2 3) '(4 5 6))  ; -> '(1 2 3 4 5 6)
(append '() '(4 5 6))  ; -> '(4 5 6)

;; normal definition
(define append
  (λ (l1 l2)
    (cond
     [(null? l1) l2]
     [else
      (cons (car l1)
            (append (cdr l1) l2))])))

(display
 (simple-format #f
                "~a\n"
                (append '(1 2) '(3 4))))

;; lets define a print
(define (print sth)
  (display
   (simple-format #f "~a\n" sth)))

(print (run 1 (q) (== q 6) (== q 5)))
(print (run 1 (q) (== q 6)))
(print
 (run* (q x y z)
      (== x 5)
      (== y x)
      (== z y)
      (== q `(,x ,y ,z))))

;; Now lets try to turn append into a relation instead of a function
;; using miniKanren!

(define appendo-attempt-1
  ;; `out` will be unified with the value of the resulting list.
  ;; Instead of returning values we are associating values with `out`.
  (λ (l1 l2 out)
    (conde
     [(== l1 '())
      ;; Here we need to associate `out` with the value of `l2`,
      ;; because `l1` has no elements to append to.
      (== l2 out)])))

(print
 (run* (q)
       (appendo-attempt-1 '() '(4 5) q)))

(print
 (run* (q)
       (appendo-attempt-1 '(1 2 3) '(4 5) q)))
;; We got the empty list, because appendo could not unify, because we
;; only have the conde clause where l1 is empty.

;; So let us define the other clauses.
(define appendo-attempt-2
  (λ (l1 l2 out)
    (conde
     [(== l1 '()) (== l2 out)]
     ;; For the else case we could write a clause that always
     ;; succeeds, for example (== 5 5). Or we could define an `elso`
     ;; to put in like that. Instead we have a goal that always
     ;; succeeds called `succeed`.  However, it is not required, as we
     ;; could simply put the relations we want to succeed there
     ;; instead.  `conde` stands for `cond` + `every`, so it is going
     ;; to try all case anyway. So we do not even need `succeed` here.

     ;; It can be difficult to express that something is not a value,
     ;; because we have only == and not `not` or `!=` or things like
     ;; that.  miniKanren is based on a search, which tries to match
     ;; things, so it is difficult to express that is should search
     ;; for not matching something.  So we need to be clever and find
     ;; a positive expression to express the opposite of matching a
     ;; value. In this case we know that we get a list as input, so
     ;; the opposite of being the empty list is being at least a pair,
     ;; assuming we really got a list.
     [(fresh (head tail result)
             (== (cons head tail) l1)
             ;; Associate cdr of the list with `tail`, explanation
             ;; below. Actually this is redundant because `tail` is
             ;; already unified to the cdr of the list by the
             ;; unification (== (cons head tail) l1). So lets comment
             ;; it out.
             #;(cdro l1 tail)
             ;; The equivalent would be:
             ;; (cdro l1 tail)
             ;; (caro l1 head)


             #; (appendo-attempt-2
              ;; We cannot take the cdr of a logic variable. So we cannot use
              ;; cdr like in the normal append definition. There is `cdro` in
              ;; miniKanren. However, `cdro` does not work like the normal
              ;; cdr. Instead it associates the cdr of a list with another
              ;; value (specifying the search space more).

              ;; `cdro` does not return a value, but we need a value for the
              ;; recursive call to appendo. So we need to pull out cdro and
              ;; use the variable it associates with the cdr of the list as
              ;; an argument. That's why we have it above this clause!
              tail
              l2
              ???)
             ;; In the normal version of append we return the value of
             ;; cons. In the relational world we need to unify out
             ;; with the value constructed by cons.
             #;(== (cons head
                       (appendo-attempt-2 tail l2 ???))
             out)
             ;; However, we cannot nest the call to appendo in the
             ;; cons. That's just miniKanren for you. So pull it out
             ;; again!
             (appendo-attempt-2 tail l2 result)  ; unification with result
             ;; and then use it in the cons to associate with out,
             ;; promoting the result of appendo to the
             ;; relationship-scoped `out` of appendo.
             (== (cons head result) out))])))

;; In short:
(define appendo-attempt-2-short
  (λ (l1 l2 out)
    (conde
     [(== l1 '()) (== l2 out)]
     [(fresh (head tail result)
             (== (cons head tail) l1)
             (appendo-attempt-2 tail l2 result)
             (== (cons head result) out))])))

;; However, if we ask this appendo for more than the possible number
;; of solutions, it will become not terminate. This is because the
;; recursive call to appendo is not in the last position. Because it
;; is not in the last position, what happens is, that ... ??? (It's
;; complicated!)  So we can see, that the order of calls inside a
;; fresh does in fact matter, which has to do with how miniKanren is
;; implemented.
(define appendo
  (λ (l1 l2 out)
    (conde
     [(== l1 '()) (== l2 out)]
     [(fresh (head tail result)
             (== (cons head tail) l1)
             (== (cons head result) out)
             (appendo tail l2 result))])))

;; Generally speaking, we can swap the following:
;; 1. == clauses
;; 2. conde clauses
;; but not the following:
;; 1. recursive calls (This is an open research problem for the authors of miniKanren!)

(print
 (run* (out)
       (appendo '() '(4 5) out)))
(print
 (run* (out)
       (appendo '(1 2 3) '(4 5) out)))

(print
 (run* (out)
       (fresh (a)
              (== a '(-1 -2))
              (appendo `(,a) '(4 5) out))))

;; We can now do persistency checks!
(print
 (run* (q) (appendo '(1 2 3) '(4 5) '(1 2 3 4 5))))
(print
 (run* (q) (appendo '(1 2 3) '(4 5) '(1 2 3 4 5 6))))

;; We can ask questions!
(print
 (run 1 (q) (appendo '(1 2 3) q '(1 2 3 4 5))))
(print
 (run 1 (q) (appendo q '(4 5) '(1 2 3 4 5))))
(print
 (run 6 (a b) (appendo a b '(1 2 3 4 5))))
(print
 (run 2 (a b c) (appendo a b c)))

;; What we are doing here is basically some type of theorem proving
;; about infinitely many values, which would not be possible with the
;; normal append.

;; We can mathematically prove, that there are no more ways to build a certain list using run*.
(print
 (run* (a b)
       (appendo a b '(1 2 3 4 5))))