How do we implement prologs findall in kanren. Prolog findall e.g:

f(X) :- findall(Y,g(Y),X)

Has the semantic to make a list of all Y solving g(Y) and put it in X. Now kanren is not minikanren, but something close to it and today much research and activity is related to minkanren and mikrokanrens.

So a predicate in kanren representing findall should be somthing like

(define (findall var code res)     
  (lambda (bindings fail cc)
     (let lp ((l '()) (env (execute-code bindings code)))
        (if env
            (let ((c-sub (car env))
                  (fail-sub     (cdr env)))
              (lp (cons (reify bindings-sub var) l) (fail-sub)))
            ((== res (reverse l)) bindings fail cc)))))

Kanren has the property that everything is not evaluated in tail contexts. Therefore we can't just add a fail thunk and a continution lambda that return data. We must be more clever and use delimited continuations, as a longjump e.g:

(define (execute-code bindings code)
  (call-with-prompt prompt-id
     (lambda ()
        (define (fail) #f)

        (define (cc bindings-sub fail-sub)
           (abort prompt-id bindings-sub)
           (fail-sub))

        (code bindings fail cc))
     (lambda (k bindings-sub) 
       (cons bindings-sub k))))

As you can see a cc continuation is a lambda that has as argumnets the resulting bindings and a failure thunk, that called will backtrack backwards from the continuation. A call-with-prompt executes the first lambda which call the code which when fails returns #f and in case code suceeds we will longjump back with the argument bindings-sub to the handler which is the second lambda that just returns (cons bindings-sub k). Here k is the continuation that when executes setup the stack with the values that kanren needs to continue and then continue to directly fail back. Then if you go back to the first code section you see that we will at the sucess return a pair where the first is the bindings, that is extracted to generate a representation of the variable var and add it to the list (there remains some trickery to do this correctly, essentially you need to modify kanren's reify to supply fresh variables in stead of symbol representations) and then execude the fail-sub to continue searching for the next solution of code. When code fails the cons list is reversed and unified with res. To use this ideom you run findall like

...
(all (forall x (g x 12)              l1) 
     (forall x (any (g x 2) (g x 7)) l2)
     ...

The solution for minikanren and microkanren is similar. As a bonus challange, make a more abstract idiom that takes a reducer argument and then define code like sum-all product-all min-all max-all etc.