Clojurians Log v2

uk does interleave, see how mplus flips streams 1 and 2

I just got it (I think) Choice is a TAKEN choice, not a possibility to choose. It's the type for head and rest of stream

yes, agree is a (lazy) stream of substitutions, although the API return substitutions by lazy implementation its holding on to goals that are yet to be executed

not a proper answer but my guess is because clojure cons is not a pair, can't hold a thunk as tail. also lazyseq uses synchronized methods to unfold, so maybe choice is more light weight. https://github.com/jasonhemann/microKanren/blob/master/microKanren.scm#L45 https://github.com/michaelballantyne/faster-minikanren/blob/master/mk.scm#L287C27-L287C27 https://github.com/clojure/core.logic/blob/master/src/main/clojure/clojure/core/logic.clj#L1092 🙂 I'm fascinated that you could also implement minikanren just with lazy-seq

;; naive implementation, todo remove nils
(defn mplus
  ([g1 g2]
   (fn [s]
     (interleave-all (g1 s) (g2 s)))))

(defn mbind [g1 & g2]
  (fn [s]
    (mapcat g2 (g1 s))))

AFAIK the lack of improper lists is the reason for LCons. So what does Choice do?

Yes but LCons is on the unification side of things. LCons is for unifying list-ish things. Choice builds a structure for holding the disjunctions of goals(predicates/relations) during the search

(ns 
  (:require [clojure.core.logic :refer :all]
            [clojure.core.logic.protocols :refer [mplus bind]]))

(run* [q]
  (conde
   [(== q 1)]
   [(== q 2)]
   [(== q 3)]))

(run* [q]
  (fn [a]
    (mplus* (bind a (== q 1))
            (bind a (== q 2))
            (bind a (== q 3)))))

(run* [q]
  (fn [a]
    (mplus (bind a (== q 1))
           (mplus (bind a (== q 2))
                  (bind a (== q 3))))))

;; leaving the interleaving aside
(run* [q]
  (fn [a]
    (->Choice ((== q 1) a)
              (fn []
                (->Choice  ((== q 2) a)
                           (fn [] ((== q 3) a)))))))

from Byrd's dissertation https://scholarworks.iu.edu/dspace/bitstream/handle/2022/8777/Byrd_indiana_0093A_10344.pdf page 51 a choice represents a stream of values. So I think is correct to say that choice is a stream of substitutions. By the way I'm not sure I fully understand the dissertation either, maybe some parts.😂

What's messing with me is although you're right I don't think the rhs of Choice should be a goal

(extend-type Object
  IMPlus
  (mplus [this f]
    (Choice. this f)))

(defn to-stream [aseq]
  (let [aseq (drop-while nil? aseq)]
    (when (seq aseq)
      (choice (first aseq)
              (fn [] (to-stream (next aseq)))))))

It behaves like a lazier lazy seq

Maybe @dnolen remembers why he wrote it over a decade ago

okay I should have referred to the mk dissertation and not uk Looks like choice is just a stream constructor

In mk it's just cons, in core.logic the important bit is implementing take*

I forget, but uk might not do interleaved search, meaning it does depth first search, where mk and core.logic does bfs

Choice is what's returned by msplit