Vacuum Fluctuations

Qi Meeting November 7 2025

Adjacent meetings: Previous | Up | Next

Summary

We explored two different approaches to formalizing Qi's binding scope rules in Redex: generalized flow values and vacuum fluctuations.

Background

Recently, Eutro completed an initial Redex implementation of Qi's formal semantics, but the handling of bindings and effects remains unspecified.

Bindings in Redex

We still didn't have a good idea of how to encode Qi's binding rules in Redex, as, although they are lexical, the scope of a binding is not textually contained within Qi's as binding form, the way it is with Racket's let (and in lambda calculus more generally).

Redex's #:refers-to mechanism for notating binding rules appears to expect a containing binding form, which appears to imply that it can only express tree-structured scope, whereas Qi's designed scoping rules are DAG-structured.

Eutro proposed one idea: avoid using this #:refers-to mechanism entirely, and instead, encode the scoping semantics as syntactic transformations involving "named" flow values that could be produced by an extended gen form (in addition to the positional flow values it already produces).

Generalized Flow Values

Eutro's key insight with this approach is that Qi bindings bind downstream flows, which is exactly the defining property of (positional) values produced by flows, and reflects the same core idea of directionality presumed by the concept of something being downstream. Thus, as this core concept is upheld in both cases, we should in principle be able to reduce the semantics of bindings, as well as the semantics of positional flow values, to the semantics of such generalized flow values that could be either positional or named.

The first step was to extend the gen form so that it can also generate named values, which could be notated (gen v ... #:var a val ...).

Then, (as v) rewrites to (gen #:var v value), and named values pass through the flow unchanged so that they are simply part of each such downstream gen. In this way, the semantics of Qi with bindings inherits the "Markov" property of regular Qi flows, where knowing the values produced by the preceding flow is sufficient to reduce the rest of the flow (a kind of referential transparency), and there is no need for nonlocal resolution of references at all.

Finally, the reduction rules for various forms need to be modified to account for the possibility of named gen's.

"Environment Algebra"

For bifurcating forms such as tee and relay, this presented some new challenges, as the bindings on each branch need to be reconciled at the end when the branches merge. This required defining a notion of an "environment," or set of bindings, along with a basic algebra for how they are modified and, in the case of such forms, unified.

Eutro first defined a simpler form of unification: shadowing. This effectively implements Qi's actual (in Qi's usual function-based Racket implementation) tree-structured binding scope in such bifurcating forms. Once this simpler set of rules is implemented, we could modify it behind the abstraction of "unification" of environments to employ some form of union instead, signaling an error if the environments bind common identifiers. This would implement Qi's designed binding rules.

After playing around with it for a while, things started to get fairly complicated. One critical issue was that once tee or relay branches were all in the form (gen v ... #:var x v ...), it was not clear which of the x-es existed before the tee/relay, and which were created in the branch, in order to implement even shadowing correctly. Consider:

(~> (gen 0) (as x) (gen 1)
    (tee (as x) (~>))
    (gen x))
;; which would ultimately reduce to:
(~> (tee (~> (gen 1 #:var x 0) (as x))
         (~> (gen 1 #:var x 0)))
    (gen x))
;; -->*
(~> (tee (gen #:var x 1)
         (gen 1 #:var x 0))
    (gen x))

In this situation, the correct reduction of the tee form would be (gen 1 #:var x 1), but the retained #:var x in the second branch would "shadow" the binding from the first branch.

We started to question whether there might be a simpler way.

Vibe is Off?

Although Sid was initially convinced by the concept of "generalized flows" that include both named and positional arguments, Dominik and Eutro increasingly had their doubts, and felt that the "vibe was off."

Dominik felt that, while some of the other approaches we've taken in these semantics, such as the introduction of gen that supports multiple values in each position (flattening them), have also stretched the Qi core language in order to make reductions convenient, that those extensions have all felt natural in some way. "They are not just theoretical tricks but feel like feature requests for Qi." On the other hand, a core form that generates named values, in some ways, circumvents the core flow-oriented paradigm.

Thinking back, Noah would probably also agree with this view, as he opined once that Qi is essentially about Cartesian Closed Categories, which are fundamentally positional. If we introduced this name-oriented gen form, we would need to imagine some form of generalization of CCC in order to exhibit the same theoretical elegance.

[!NOTE] Eutro: I think this would actually work just fine in a CCC, it might even be the best approach for Qi's denotational semantics (up to un/currying, perhaps). I also suspect that denotational semantics for Qi would be simpler and more natural than the operational semantics, but I'm not volunteering my time at the moment.

The Space Between

Dominik sketched an alternative approach that could avoid introducing the name-oriented gen, and would rely on Redex's #:refers-to facility.

He suggested that since all flows reduce to gen in the semantics, even bifurcating ones like tee, though the flow is internally nonlinear, we should be able to derive, upon reduction, some form of "linearization" of the flow that would be expressed purely in terms of successive gen's inside a ~>. Then at that point, if that were possible, we should be able to use #:refers-to, as the binding structure could then be expressed as tree-structured scope.

Sid was initially skeptical, since this seems to hinge on whether Qi flows can in general be linearized — for any flow f, does there always exist a linear flow g that is equivalent to it? "Equivalence" here would likely need to be defined in relation to a formal semantics accounting for both output and effects, rather than just whether the same value is computed by both flows. And on the face of it, this appears to be a rabbit hole.

But whether the flow itself could be expressed linearly and whether the semantic reductions could be expressed linearly could be two different things. Additionally, although the bindings along each tine of a branching flow are independent, there is one constraint: they cannot bind the same identifiers. This could also simplify the problem of "linearizing" the flow.

Dominik had an insight into an approach we could take to encoding the semantics, which is that at the end of the junction when it reintegrates into the main stream, there is a "space between" that point and downstream flows where we could introduce arbitrary computations ("vacuum fluctuations," if you will), by employing:

(~> ... ▽ (as vs) ⏚ f∅ ... (gen vs) △ ...)

That is, collect the values at a certain point in the flow and then ground them, but not before first binding them so they're available downstream to be produced once more from the void.

Additionally, we can always translate between flow values and named values:

;; flow values → named values
(~> f ... (as x y z))
(~> f ... ▽ (as vs))

;; named values → flow values
(~> f ... (as x y z) (gen x y z))

These devices give us a lot of power. The question now is, can we use them to capture the distinct bindings on the separate branches, encoding this DAG binding structure in Redex's linear, tree-structured binding notation language?

Trying the Second Approach

Dominik said he would continue with the second ("vacuum fluctuations") approach and see if he can get it to work. He plans to first implement scoping rules for a simpler language than Qi and then gradually make the language resemble Qi by introducing the nonlinear forms, etc., to see what challenges will be revealed.

Eutro suggested that we might be able to use utilities from Redex like apply-reduction-relation/try-with-names to get information about which reduction rule was applied at each step, which could approximate the conveniences we are used to with the Macro Stepper.

Commonalities and Directions

In either approach, each flow ultimately (1) produces flow values and (2) creates bindings.

We haven't yet talked about effects. It's likely that that will be a third component here.

We also haven't talked about first class continuations in Qi recently. It's possible they would have distinct handling from ordinary effects, and that could be yet another aspect to develop as we formalize the complete semantics of Qi.

Vlibench Breaks on Racket 9.0??

Sam pointed out on Discord that vlibench (which generates the rigorous competitive benchmark reports displayed on the Qi source repo, which are run on every commit to the main branch) was one of the packages found to have build failures on the upcoming Racket 9.0 branch.

Dominik investigated and discovered that the problem was caused by a change in hardware in the build environment rather than by a change in Racket. Specifically, formerly, Racket builds were being done on x86_64 CPUs, but now they're being built on ARM64 emulating x86_64. This ends up reporting hardware information in a different format than the library was expecting, causing us to attempt passing a #false value to the Scribble function racketfont, which was then complaining as it expects a string.

Finding a standard representation of CPU information across diverse CPUs and operating systems proved to be surprisingly hard, as even the same CPU information is reported differently on different operating systems. Dominik wrote a helper function, get-cpu-info-string, which gracefully handles this case now, correctly reporting CPU information and avoiding the error in case that information is unavailable.

In any case, the failure on Racket 9.0 is just a coincidence, and likely, the build environment was changed as part of other improvements towards the Racket 9.0 release.

For a Given Value of Fun

Rocky Horror Picture Show

Sid plans to watch Rocky Horror Picture Show soon, finally, so that he can finally get Dominik's references to it.

Univalent Foundations of Qi

We discussed formalisms supporting call-by-value and call-by-name semantics, and how "univalent duploids" allow mixing both, enabling the expression of inlining in an otherwise call-by-value semantics. This sounded relevant to Qi as it's a call-by-value language that needs to do inlining.

Zed Eff See

Sid grew up saying "zed" and now says "zee." It's among the Americanisms (along with Fahrenheit) that he's convinced by, on the basis that "zee" rhymes, in the song. Eutro opined that the song doesn't have well-defined metre anyway, and so rhyming is irrelevant.

It turns out, truth is stranger than fiction.

Precious Rabbit Holes

We've all been tied up with things lately, and many of our most precious rabbit holes lie unexplored, from Dominik's terminal-based 3d renderer, to Sid's (allegedly) main work on economics, to Eutro's One Emacs Package Manager to Rule them All.

Well, the light is visible at the end of some rabbit holes at least, the holidays and term's end are approaching, and we hope we'll have more free time soon.

RacketFest '26?

Dominik is floating the idea of hosting RacketFest '26 in Prague with his university colleagues, and there is some interest! He even has contacts in a student group in the area that he helped start years ago, which could handle the AV for the conference. Sometime in Spring '26 just might be possible.

Next Steps

(Some of these are carried over from last time)

• Add bindings and effects to the Redex semantics.
• Incorporate Chai into Qi.
• Implement a compile-time table of known arities and add an entry to it as part of define-flow.
• Ready the inlining PR to be merged and tag for code review.
• Write phase 1 unit tests for inlining.
• Define the define-producer, define-transformer, and define-consumer interface for extending deforestation (also encapsulating both naive and stream semantics in the definition), and re-implement existing operations using it.
• Implement the remaining producers and transformers in racket/list for qi/list.
• Attach a deforested syntax property in the deforestation pass, and use it in compiler rules tests (instead of string matching).
• Improve qi/list and deforestation testing by writing a macro to simultaneously test the expansion and the semantics.
• Investigate whether the deforested operations could be expressed using a small number of core forms like #%producer, #%transformer, #%consumer, and #%stream.
• Decide on whether there will be any deforested operations provided in (require qi) (without (require qi/list))
• Review which racket/list forms are actually needed in qi/list
• Come up with a good way to validate the syntactic arguments to range using contracts.
• Start organizing qi-lib into qi and qi/base collections
• Publish qi/class in some form.
• Implement DAG-like binding rules for branching forms [Syntax Spec parallel binding-spec PR]
• Formalize Qi's semantics using Redex.
• Incorporate effects and bindings into Qi's pen-and-paper semantic model.
• Return to developing Qi's theory of effects, including accounting for binding rules.
• Write a proof-of-concept for implementing code generation from abstractions of "flow" and "connective tissue" that are set by a context parameter.
• Why is range-map-car slower against Racket following the Qi 5 release?
• Decide on appropriate reference implementations to use for comparison in the new benchmarks report and add them.
• Add reader flow syntax in #lang qi
• Develop a backwards-incompatibility migration tool using Resyntax, to be used in the next Qi release.

Attendees

Dominik, Eutro, Sid