guile-minikanren-uncourse-code/membero.scm

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

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

;; and a more special answers printing print-answers
(define (print-answers answers)
  (define (iter answers count)
    (cond [(null? answers) (print "That's all of them.")]
        [else
         (print (simple-format #f "  ~a: ~a" count (car answers)))
         (iter (cdr answers) (+ 1 count))]))
  (print "Answers:")
  (iter answers 1))

;; normal member function
(print (member 5 '(3 4 5 6 7)))  ; -> (5 6 7)
(print (member 5 '(3 4 5 6 5 6 7)))  ; -> (5 6 5 6 8)
(print (member 15 '(3 4 5 6 5 6 7)))  ; -> #f

;; Lets try to write membero!  To start define member in scheme, maybe
;; we can again translate from it to miniKanren's membero.
(define member
  (λ (elem lst)
    (cond
     [(null? lst) #f]
     [(equal? (car lst) elem) lst]
     [else
      (member elem (cdr lst))])))

(print (member 5 '(3 4 5 6 7)))  ; -> (5 6 7)
(print (member 5 '(3 4 5 6 5 6 7)))  ; -> (5 6 5 6 8)
(print (member 15 '(3 4 5 6 5 6 7)))  ; -> #f

;; Lets move towards membero.
(define membero-attempt-1
  (λ (elem lst out)
    (conde
     [(== '() lst) (== out #f)]  ; or use nullo, which does the same
     [(fresh (head tail)
             ;; You could use caro, which does the same as the following.
             ;; "deconstructor" cons, sort of like pattern matching
             (== (cons head tail) lst)
             (== head elem)  ; if the car of the pair (head of the list) is elem, elem is a member
             (== out l))]  ; unify the out variable with the list as a result
)))
;; Since we are unifying the head of the list with elem, we could
;; optimize here and put elem into the destructuring cons unification.

(define membero-attempt-2
  (λ (elem lst out)
    (conde
     [(== '() lst) (== out #f)]
     [(fresh (tail)
             (== (cons elem tail) lst)
             (== out lst))]
     [(fresh (head tail)
             (== (cons head tail) lst)
             (membero-attempt-2 elem tail out))])))

(print
 (run 1 (q)
      (membero-attempt-2 5 '(3 4 5 6 7) q)))
(print
 (run 2 (q)
      (membero-attempt-2 5 '(3 4 5 6 5 6 7) q)))
(print
 (run* (q)
      (membero-attempt-2 5 '(3 4 5 6 5 6 7) q)))

(print-answers
 (run* (q)
       (membero-attempt-2 5 '(3 4 5 6 5 6 7) q)))

;; That query gave multiple answers. But those cannot be all true at
;; the same time. An element cannot be member of a list and at the
;; same time not be a member of the list. No Schrödinger-ing now
;; please! Why is this happening?

;; Our conde clauses are overlapping! They are not mutually exclusive!
;; That's because conde will try all subexpressions and we do not have
;; the implicit negation from the normal scheme cond from the member
;; function in out miniKanren version of membero.

;; So lets introduce those implicit negations as explicit negations in
;; our miniKanren membero code.

(define membero-attempt-3
  (λ (elem lst out)
    (conde
     [(== '() lst) (== out #f)]
     [(fresh (head tail)
             ;; In the Scheme version of member, there would be an
             ;; implicit test here, which says: If we get a list and
             ;; the condition of the first clause of cond is not true,
             ;; then the list is not empty, so we have at least a
             ;; pair.  In miniKanren we would have to write that test
             ;; explicitly as follows ...
             (== (cons head tail) lst)
             ;; ... and then progress as before.
             (== (cons elem tail) lst)
             (== out lst))]
     [(fresh (head tail)
             (== (cons head tail) lst)
             (membero-attempt-3 elem tail out))])))

;; However, we already have a destructuring unification with cons in
;; there, so we actually already have that test covered. This means we
;; do not need to add the test.
(define membero-attempt-4
  (λ (elem lst out)
    (conde
     [(== '() lst) (== out #f)]
     [(fresh (tail)
             ;; This fine.
             (== (cons elem tail) lst)
             (== out lst))]
     [(fresh (head tail)
             ;; Here however, we are not expressing, that the head of
             ;; the list is not equal to the element we are looking
             ;; for. That is a problem. We would like to write
             ;; something like (=/= head elem) and there actually _is_
             ;; =/= in miniKanren. Let's use it.
             (=/= head elem)
             (== (cons head tail) lst)
             (membero-attempt-4 elem tail out))])))

(print-answers
 (run* (q)
       (membero-attempt-4 5 '(3 4 5 6 5 6 7) q)))
(print-answers
 (run* (q)
       (membero-attempt-4 100 '(3 4 5 6 5 6 7) q)))

;; We get back #f for trying to find members that are not in the
;; list. The problem with that is, that #f will be an answer for the
;; query and it could mean something like "The element you are looking
;; for is in the sublist #f.". In this case #f is not a sublist and it
;; would still be clear, but in other cases such an answer could be
;; confusing and difficult to interpret correctly. To fix this kind of
;; behavior, we could simply remove the case, where we unify the
;; output variable out with #f. We could remove the base case.
(define membero-attempt-5
  (λ (elem lst out)
    (conde
     [(fresh (tail)
             (== (cons elem tail) lst)
             (== out lst))]
     [(fresh (head tail)
             (=/= head elem)
             (== (cons head tail) lst)
             (membero-attempt-5 elem tail out))])))

(print-answers
 (run* (q)
       (membero-attempt-5 5 '(3 4 5 6 5 6 7) q)))
(print-answers
 (run* (q)
       (membero-attempt-5 100 '(3 4 5 6 5 6 7) q)))

;; This is what we want for now, so now really define membero.
(define membero membero-attempt-5)
(print-answers
 (run* (q)
       (membero 5 '(3 4 5 6 5 6 7) q)))
(print-answers
 (run* (q)
       (membero 100 '(3 4 5 6 5 6 7) q)))