Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Questions and feedback on lang.md #11

Open
iambrj opened this issue Sep 5, 2023 · 0 comments
Open

Questions and feedback on lang.md #11

iambrj opened this issue Sep 5, 2023 · 0 comments

Comments

@iambrj
Copy link

iambrj commented Sep 5, 2023

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

We introduce the following forms.
- `staged`
- `later`
- `defrel/staged`
- `gather`

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?

In relational staging, we are partitioning the computation into goals that should happen at staging-time and goals that should happen at runtime.

Is happening of a goal same as applying 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.

It doesn't work if the program is not fully known.

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

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.

(run 4 (e v) (staged (ms-eval-ambo `(cons (amb 1 2) ,e) v)))

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

(defrel-partial (apply-lambda-ambo rep [x e env] [arg v])

I'm lost on what rep is?

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?

#### 3.2 how to stage lambda

I look forward to the documentation of the rest of Section 3!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant