namin / staged-minikanren

staged relational interpreters: running with holes, faster

staged-miniKanren

A novel framework for staging interpreters written as relations, in which the programs under interpretation are allowed to contain holes representing unknown values. We apply this staging framework to a relational interpreter for a subset of Racket, and demonstrate significant performance gains across multiple synthesis problems.

Installation

• git submodule init
• git submodule update
• Install https://github.com/michaelballantyne/syntax-spec

Running

• racket tests/all.rkt
• racket tests/all-bench.rkt

staged-minikanren's Issues

Questions and feedback on lang.md

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

staged-miniKanren/docs/lang.md

Lines 36 to 40 in a6bfb3a

	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.

staged-miniKanren/docs/lang.md

Line 42 in a6bfb3a

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?

staged-miniKanren/docs/lang.md

Line 77 in a6bfb3a

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?

staged-miniKanren/docs/lang.md

Line 79 in a6bfb3a

`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.

staged-miniKanren/docs/lang.md

Lines 101 to 102 in a6bfb3a

	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.

staged-miniKanren/docs/lang.md

Line 108 in a6bfb3a

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

staged-miniKanren/docs/lang.md

Lines 127 to 129 in a6bfb3a

	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?

staged-miniKanren/docs/lang.md

Line 148 in a6bfb3a

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.

staged-miniKanren/docs/lang.md

Line 175 in a6bfb3a

(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

staged-miniKanren/docs/lang.md

Line 221 in a6bfb3a

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

I'm lost on what rep is?

staged-miniKanren/docs/lang.md

Line 230 in a6bfb3a

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.

staged-miniKanren/docs/lang.md

Line 240 in a6bfb3a

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?

staged-miniKanren/docs/lang.md

Line 312 in a6bfb3a

#### 3.2 how to stage lambda

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

Gerbil Scheme Support Possible?

I see that there is already Racket, Guile, and Chez support for this project. Would it be possible to get Gerbil Scheme support as well?

Eliminate a relation call and re/destructuring pattern match?

It looks to me like, knowing that what you have is a cons, you can specialize the code in these cases to the non-variable cons case, and avoid restructuring the list of clauses. Am I missing something?

staged-miniKanren/staged-interp.scm

Line 592 in 4b2dff8

((match-checko (cons clause clauses))

Bug with lifting of staged code

This following works fine:

(let ([y 0])
  (run 1 (x)
    (== x y)))

But this gives an error:

(let ([y 0])
  (run 1 (x)
    (staged
      (== x y))))

The error it gives is:

variable y_10 is not bound
Context (plain):
 ~/Code/staged-miniKanren/private/faster-minikanren/mk.scm:354:7 
~Code/staged-miniKanren/private/faster-minikanren/mk.scm:317:9 
 ~/Code/staged-miniKanren/private/faster-minikanren/mk.scm:322:0 take

(Likely related to our use of syntax-local-lift-expression)