You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
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.
We want to _stage_ the interpreter: specializing the interpreter `eval-ambo` with respect to an expression `e` (the first argument of the interpreter) in the first stage. The result of specialization is miniKanren code, without the interpretive overhead of the interpreter (for example, the interpreter loop has gone away). In the second stage, we run the generated miniKanren code.
What exactly does "miniKanren code" mean in "The result of specialization is
miniKanren code, ..."? A goal expression? A goal?
`later`: `(later <goal>)` defers the goal to the second stage (runtime). In a staged interpreter, we maintain the invariant that unifications with the resulting value (the `v` argument of the interpreter) are deferred to the second stage.
Is the invariant a convention or is the invariant required to maximize the
benefits of staging? Some context about the invariant would be helpful.
To elaborate, the `(staged <goal>)` form from the example takes a goal that runs at staging-time.
It does both steps of running the first stage, and the second stage resulting from running the first stage.
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.
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):
When we define a relation with `defrel/staged`, we generate both the staged and runtime version. We get the runtime version by removing the `later` annotations.
Here the runtime version of `ms-eval-ambo` would be identical to the `eval-ambo` relation we saw in section 1.
What happens to the gather annotations? Are they erased as well?
Our approach is to try evaluating the generator interpreter and see if it's non-deterministic.
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.
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.
When creating a closure, the interpreter partially applies this new relation, using `partial-apply`. The first argument unifies with the first-class representation. The second argument is the relation name. The remainder are the first-application arguments.
When applying a closure, we `finish-apply` this relation. The first argument is the first-class representation, the second argument is the relation name, and the remaining arguments are the arguments to finish the application.
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?
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 alater
for getting the mostperformance out of staged-miniKanren.
Section 1
staged-miniKanren/docs/lang.md
Lines 36 to 40 in a6bfb3a
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.
staged-miniKanren/docs/lang.md
Line 42 in a6bfb3a
What exactly does "miniKanren code" mean in "The result of specialization is
miniKanren code, ..."? A goal expression? A goal?
staged-miniKanren/docs/lang.md
Line 77 in a6bfb3a
Is happening of a goal same as applying a goal?
staged-miniKanren/docs/lang.md
Line 79 in a6bfb3a
Is the invariant a convention or is the invariant required to maximize the
benefits of staging? Some context about the invariant would be helpful.
staged-miniKanren/docs/lang.md
Lines 101 to 102 in a6bfb3a
I find it confusing that the generated "miniKanren code" must be passed to
staged
rather than used in arun
/run*
. For example, if(== 1 2)
fits thedefinition of "miniKanren code",
(== 1 2)
can be used in arun
/run*
. Ithink this arises from my lack of clarity on what "generated miniKanren code"
means.
staged-miniKanren/docs/lang.md
Line 108 in a6bfb3a
It is unclear to me why it doesn't work. For example, if I have a goal
two-or-three
:and I run
two-or-three
with a fresh variable, I expect miniKanren to returnpossible values for the fresh variable:
so why does running
gen-eval-ambo
with fresh variables not produce possiblevalues 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
ingen-eval-ambo
is searched for answers):Nitpick: Using
gen-eval-ambo
instead of "it" in "It doesn't work ..." would beclearer.
Section 2
staged-miniKanren/docs/lang.md
Lines 127 to 129 in a6bfb3a
What happens to the
gather
annotations? Are they erased as well?staged-miniKanren/docs/lang.md
Line 148 in a6bfb3a
Does "generator interpreter" mean the specialized generated interpreter? So far
in Section 2 I've gathered that
defrel/staged
produces two interpreters: theunspecialized runtime interpreter and specialized generated interpreter. I'm
unsure what the "generator interpreter" is.
staged-miniKanren/docs/lang.md
Line 175 in a6bfb3a
Is the output of this line missing?
Again, it is unclear to me what the input/output types of
fallback
are andhow/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 2more comprehensible.
Section 3
staged-miniKanren/docs/lang.md
Line 221 in a6bfb3a
I'm lost on what
rep
is?staged-miniKanren/docs/lang.md
Line 230 in a6bfb3a
staged-miniKanren/docs/lang.md
Line 240 in a6bfb3a
I feel I don't fully understand the semantics of
partial-apply
andfinish-apply
. Are they variadic relations that can be used with any partiallyapplicable relation? Or are they defined specifically only to implement closures
in
apply-lambda-ambo
?staged-miniKanren/docs/lang.md
Line 312 in a6bfb3a
I look forward to the documentation of the rest of Section 3!
The text was updated successfully, but these errors were encountered: