Questions and feedback on lang.md

[iambrj]

High-level feedback

I felt informed on the new forms staged-miniKanren introduces, but I don’t understand where and how to use each of them. For example, I don’t know which == goal expressions need to be wrapped in a later for getting the most performance out of staged-miniKanren.

Section 1

https://github.com/namin/staged-miniKanren/blob/a6bfb3a1f3076a03da0e1014ab87375318aa7f88/docs/lang.md?plain=1#L36-L40 I feel definitions and input/output types along with the form names would make Section 1 more comprehensible. I am unsure after reading Section 1 on what each of them exactly does.

https://github.com/namin/staged-miniKanren/blob/a6bfb3a1f3076a03da0e1014ab87375318aa7f88/docs/lang.md?plain=1#L42 What exactly does "miniKanren code" mean in "The result of specialization is miniKanren code, ..."? A goal expression? A goal?

https://github.com/namin/staged-miniKanren/blob/a6bfb3a1f3076a03da0e1014ab87375318aa7f88/docs/lang.md?plain=1#L77 Is happening of a goal same as applying a goal?

https://github.com/namin/staged-miniKanren/blob/a6bfb3a1f3076a03da0e1014ab87375318aa7f88/docs/lang.md?plain=1#L79 Is the invariant a convention or is the invariant required to maximize the benefits of staging? Some context about the invariant would be helpful.

https://github.com/namin/staged-miniKanren/blob/a6bfb3a1f3076a03da0e1014ab87375318aa7f88/docs/lang.md?plain=1#L101-L102 I find it confusing that the generated "miniKanren code" must be passed to staged rather than used in a run/run*. For example, if (== 1 2) fits the definition of "miniKanren code", (== 1 2) can be used in a run/run*. I think this arises from my lack of clarity on what "generated miniKanren code" means.

https://github.com/namin/staged-miniKanren/blob/a6bfb3a1f3076a03da0e1014ab87375318aa7f88/docs/lang.md?plain=1#L108 It is unclear to me why it doesn't work. For example, if I have a goal two-or-three:

(define (two-or-three x)
  (conde
    [(== 2 x)]
    [(== 3 x)]))

and I run two-or-three with a fresh variable, I expect miniKanren to return possible values for the fresh variable:

(run 2 (v) (two-or-three v))
;; => (2 3)

so why does running gen-eval-ambo with fresh variables not produce possible values for the fresh variables? For example, some possible answers according to my miniKanren mental model could be (modulo order, assuming the first branch of the outer conde in gen-eval-ambo is searched for answers):

(run 2 (e v) (staged (gen-eval-ambo `(cons (amb 1 2) ,e) v)))
;; => (((1 . _.0) (num _.0)) ((2 . _.0) (num _.1)))

Nitpick: Using gen-eval-ambo instead of "it" in "It doesn't work ..." would be clearer.

Section 2

https://github.com/namin/staged-miniKanren/blob/a6bfb3a1f3076a03da0e1014ab87375318aa7f88/docs/lang.md?plain=1#L127-L129 What happens to the gather annotations? Are they erased as well?

https://github.com/namin/staged-miniKanren/blob/a6bfb3a1f3076a03da0e1014ab87375318aa7f88/docs/lang.md?plain=1#L148 Does "generator interpreter" mean the specialized generated interpreter? So far in Section 2 I've gathered that defrel/staged produces two interpreters: the unspecialized runtime interpreter and specialized generated interpreter. I'm unsure what the "generator interpreter" is.

https://github.com/namin/staged-miniKanren/blob/a6bfb3a1f3076a03da0e1014ab87375318aa7f88/docs/lang.md?plain=1#L175 Is the output of this line missing?

Again, it is unclear to me what the input/output types of fallback are and how/when I must use it if I write staged miniKanren code. Should all code that can potentially run "backwards" with non-determinism be wrapped in a fallback? I feel a definition and input/output types of fallback would make Section 2 more comprehensible.

Section 3

https://github.com/namin/staged-miniKanren/blob/a6bfb3a1f3076a03da0e1014ab87375318aa7f88/docs/lang.md?plain=1#L221 I'm lost on what rep is?

https://github.com/namin/staged-miniKanren/blob/a6bfb3a1f3076a03da0e1014ab87375318aa7f88/docs/lang.md?plain=1#L230 https://github.com/namin/staged-miniKanren/blob/a6bfb3a1f3076a03da0e1014ab87375318aa7f88/docs/lang.md?plain=1#L240 I feel I don't fully understand the semantics of partial-apply and finish-apply. Are they variadic relations that can be used with any partially applicable relation? Or are they defined specifically only to implement closures in apply-lambda-ambo?

https://github.com/namin/staged-miniKanren/blob/a6bfb3a1f3076a03da0e1014ab87375318aa7f88/docs/lang.md?plain=1#L312 I look forward to the documentation of the rest of Section 3!