Many Worlds

Qi Meeting Nov 14 2025 and Nov 21 2025

Adjacent meetings: Previous | Up | Next

Summary

We discussed a difficulty we encountered last week with handling bindings in bifurcating flows such as tee junctions, and a proposed resolution. We also discussed the meaning of ambiguity in Qi more generally. We also discussed a potential difficulty stemming from propagating an environment in our working semantics, Cartesian Closed Categories as a theoretical foundation for Qi, the change in weather, and other things.

NOTE: These are combined notes from Nov 14 and Nov 21.

Background

Last week, we explored two approaches to formalizing the semantics of bindings in Qi. We encountered some challenges there, including especially the handling of bindings in tee junctions and other forking forms.

Bad Vibes?

We should first make note of one correction. Last week, we had started to feel that the "vibe" of the "generalized flow values" approach to formalizing bindings was "off" — that extending the core gen form to produce named values in addition to flow values seems to move us away from the core flow-oriented paradigm.

But upon further reflection, the formalization is only guilty of confronting us with the fact that the introduction of bindings already deviates from the core flow-oriented paradigm. Original sin has already been committed, and this formalization is just revealing the essence of the language to have been altered, by this act of introducing bindings, to the "generalized" flow-oriented form, where named values may be produced while still respecting a more abstract flow-orientation. So whether the vibes are off is more properly a meta-discussion about the introduction of bindings to Qi rather than about this particular formalization of them. Of course, if vacuum fluctuations or another approach proves to be simpler, that's another matter, but it does not appear that there is anything essentially off about GFV, either.

Regarding the "original sin," we discussed after the meeting that there has in fact been an alternative to bindings that has been discussed before, "bingdi (并蒂)" (fittingly, almost an anagram of "binding"!) aka "Yin/Yang symmetry," which addresses (and provides an alternative to) a prominent use of bindings in Qi to curry flows for subsequent application.

Giving Meaning to Ambiguity

Now, with that out of the way, let's return to the difficulty we encountered last week. Consider the following flow:

    → T₁ →
   /      \
U →        → D
   \      /
    → T₂ →

U is upstream of a fork (e.g., a tee junction) with tines T₁ and T₂, which are upstream of D.

In the generalized flow values approach, every flow reduces to a generalized gen capable of producing both ordinary flow values as well as named values. Thus, each of the component flows above reduces to gen (as does the entire flow, eventually).

gen is "Markov" in the sense that it obscures — and in our working semantics, abstracts — all upstream information about the flow as a simple production of values at that specific point. This includes both flow values as well as named values, leveraging the insight that named values exhibit flow structure, too. Yet, if a tine of a bifurcating flow (e.g., T₁ above) rebinds an identifier bound upstream (e.g., in U), then presumably, one of these should take precedence over the other — otherwise the binding would be ambiguous. However, a "Markov" gen loses the information about whether the binding was merely carried forward from an upstream binding or subsequently rebound in a tine, so it does not contain sufficient information to resolve the binding.

Towards resolving this, Sid suggested on Discord:

sid — 11/14/25, 11:31 AM One resolution could be that if two tines of -< binding the same identifier is undefined, then tines rebinding an upstream identifier should also be undefined, since, downstream, the binding could be considered ambiguous depending on which path to a binding we take, looking upstream

sid — 11/14/25, 11:41 AM Another wild answer is that the entire flow has two independent meanings: (values 0) and (values 1), or, as effects may also be involved, something like ((values 0), (effects ∅)) and ((values 1), (effects ∅)). But probably just considering this case ambiguous and raising an error in "one world" would be easier 😆

Two Types of Ambiguity

Considerations of "many worlds" only come into play in cases where either:

1. Multiple values are passed in a single position, or, as we are now discovering,

2. There are ambiguous bindings involved.

These are the two forms of ambiguity that we encounter in Qi.

In the common case where flows are conveying single values via each single-valued continuation (e.g., (add1 (values 1)), or (+ (values 2) (values 3))), there is no ambiguity, as the ordinary flow values here are conveyed directly and positionally.

In the case of multiple values passed to a single-valued position (e.g., (add1 (values 0 1)), or (+ (values 1 2) (values 3))), Sid proposed one idea some time ago, to fork evaluation so that the many worlds are evaluated independently, potentially while also providing ways to manipulate and reconcile these independent computations within the language itself (for example, a reconcile form, which could be used, if we wish, to flatten the many worlds, giving us the version of gen we have been using in our formal semantics). We have yet to broach such issues in Qi development, and it is probably still years away.

But with Eutro's recent observation that bindings follow a generalized flow structure, too, it is apparent that such "named" flow values, which are conveyed logically rather than positionally, entail an analogous form of ambiguity which presents precisely the same options for resolution:

The Three Interpretations

1. Independently evaluate the many worlds ("The Many Worlds Interpretation")

2. Arbitrarily select one of the possibilities, resolving global constraints to produce a consistent value ("The Copenhagen Interpretation")

3. Raise a compile-time error signaling ambiguity. ("The Classical Interpretation)

These options apply to all cases of ambiguity discussed above (regardless of how we define ambiguity). The second (Copenhagen) option greatly resembles Scheme's amb operator.

Keepin' It Classical

Of these options, "many worlds" seems like a great candidate for implementation using parallel threads or futures (which should compose with any choice of flow backend), the "Copenhagen" interpretation seems less gratuitous and has precedent in the Scheme world, while raising the compile-time error (the Classical interpretation) seems the safest and simplest for now!

Keeping things classical is consistent with how we're already handling multiple values in a single position (which raises an error) as well as our plans for ambiguous bindings (however that's defined), and any future "quantum" explorations would remain consistent with Qi's behavior in the classical realm aside from giving meaning to ambiguity instead of raising an error.

Beyond Set of Scopes

In discussion of the specific choices for defining ambiguous bindings, Eutro observed that it would be difficult --- perhaps impossible --- to express the proposed scoping structure (viz., to consider rebinding an upstream binding in just one tine of a branching flow to be ambiguous) using the set-of-scopes model used to actually implement scoping rules in Qi.

That is, at the point where the flow bifurcates, our strategy with the parallel binding spec was to attach the upstream scope separately to each tine of the junction, and then attach the scopes from every tine downstream.

In this approach, if two tines rebind the same identifier, the binding is considered ambiguous and it is raised as a compile-time error. The ambiguous binding is signaled simply because the scope sets on the bindings in each tine are subsets of the scope set on the downstream reference, and neither tine set is a subset of the other. Set of scopes considers this ambiguous --- which is just what we want here.

On the other hand, if only one tine rebinds an upstream identifier, then set of scopes — via the parallel binding spec — would consider it to shadow the upstream binding, and it would not be considered ambiguous.

The issue that Eutro pointed out with the proposed binding structure (which attempts to redeem the GFV semantics) is that the ambiguity we are describing — of a tine being disallowed from shadowing upstream bindings — cannot be encoded as an ambiguity in set of scopes.

To elaborate, recalling the example flow from earlier:

    → T₁ →
   /      \
U →        → D
   \      /
    → T₂ →

The basic rules we've already adopted are:

• U binds T₁, T₂ and D
• T₁ and T₂ bind D
• If T₁ and T₂ bind the same identifier, the binding is ambiguous wrt. D (compile error)

All this is within set of scopes' capacity to express (and implemented by the proposed parallel binding spec).

In addition, we are considering:

• If either T₁ or T₂ shadow U, the binding is ambiguous wrt. D (compile error)

With the parallel binding spec, if T₁ shadows U, then, as U ⊂ T₁ and T₁ ⊂ D, and further, as the set of scopes on U and T₂ are identical, T₁ (as the maximal subset) is found to bind D and there is no ambiguity detected.

In order to describe an ambiguous binding structure using set of scopes, we need a set A₁ ⊂ B and another A₂ ⊂ B where A₁ and A₂ are incomparable.

One way we could do it is to attach a fresh scope associated with each upstream binding on every bifurcation, even if there isn't a fresh binding on that tine. That is, something resembling:

    → (as+ v) T₁ →
   /               \
U →                 → D
   \               /
    → (as+ v) T₂ →

Where as+ is a version of as that simply attaches a fresh scope to an identifier, retaining the binding as is. In a way, this mimics what GFV's gen does.

Now, if T₁ rebinds v, then downstream in D, set of scopes would detect the ambiguous binding as there is a fresh scope on every tine, ensuring that tines are mutually incomparable though separately subsets of the scope set on the downstream reference.

There's just one problem. This would mean that a reference following a junction is always ambiguous, unless there is a fresh antecedent binding after the junction, i.e., references must always have a linear path back to bindings.

Eutro had likely anticipated such issues, as the initial proposal had prompted her to respond on Discord that, at that point, we might as well disallow shadowing entirely (which does not seem desirable).

Additionally, this approach would complicate compilation of branching forms, necessitating the addition of tine-specific "rescoping" of all upstream identifiers!

Adopted Scoping Rules

After discussion, we agreed that retaining the rule that downstream bindings shadow upstream ones — i.e., the behavior implemented by the parallel binding spec — is the right choice.

This is the most intuitive, is what the user would expect, and also happens to be expressible using set of scopes (as the parallel binding spec proves).

What does this imply for handling "ambiguity"?

These adopted scoping rules define ambiguity with respect to binding (which is one of the two forms of ambiguity). They say that downstream bindings shadow upstream ones (i.e., there is no ambiguity here), and that the binding of an identifier that is separately bound in tines of a junction (i.e., neither downstream of the other) is ambiguous downstream.

As discussed earlier, ambiguity currently means an error (the Classical interpretation), but it may be worthwhile to revisit this interpretation somewhere down the road.

So the problem still remains

Can we modify our GFV semantics to express the desired shadowing in this case?

Do all hopes rest on vacuum fluctuations?

Or is there any fundamental limitation in Redex that would prevent encoding DAG-structured scoping rules in it at all? Michael did seem to suggest this, but it may have been specifically in the context of the #:refers-to mechanism, rather than a custom approach such as GFV that doesn't use Redex's bindings facilities.

Environment Algebra Leads to Weaker Semantics?

Michael stopped by to share his reaction to recent meeting notes describing the GFV approach, and specifically the "environment algebra," where each flow carries an environment made up of antecedent bindings.

He shared the concern that if not done carefully, this kind of carried environment could describe a weaker semantics than Qi's actual semantics, where bindings are available not only lexically but also dynamically (in contrast to Qi, where it's only lexical). He provided a counterexample that could be used as a test to validate the semantics:

;; Good use of x
(flow (~> (5) (as x) (gen x)))

;; x shouldn't be visible
(define-flow f
  x)
(flow (~> (5) (as x) f))

Categorical Curiosities

Cartesian Closed Categories

We've (esp. Noah) discussed these before, and Eutro might be learning more about them for her thesis. They might be a good semantic model to use in a denotational semantics for Qi.

First, to motivate some terminology: The set of all functions from A to B has cardinality nᵐ, where m and n are the sizes of the sets A and B, respectively (proof: for each a ∈ A, there are n choices in B, and there are m choices of a, giving n × n × ... (m times) as the size of the set of all functions, denoted Bᴬ). The set of all functions from A to B is thus called an "exponential object" (in the category of sets).

A cartesian closed category is a category:

• with product (i.e., for any objects A and B, we have another object A × B whose first and second projections are A and B, respectively)
• with exponential object (i.e., for any objects A and B, we have another object Bᴬ, e.g., the set of all functions between them)

We could imagine every object in this category as a type. For example, if we reify the object as a set, we could imagine that it is the set of all values of that type — thus, a morphism in this category is just an ordinary function from one type to another, and the relevant "exponential object" here is just the set of all functions between these two types, or equivalently, the type (-> T₁ T₂). This category has the known property that any morphism in it can be written as a lambda term in Simply-Typed Lambda Calculus. That this also implies that any morphism can be expressed as a Qi flow, and vice versa, is an exercise left to the reader.

Note: I haven't verified these definitions — just summarizing and elaborating on what I recall from our discussion!

Freyd Categories

Eutro mentioned that she is currently exploring using duploids as a univalent foundation for proofs about when inlining can and cannot be done in a compiler. Inlining essentially embeds call-by-name semantics (i.e., the variable when inlined is separately evaluated everywhere that it is inlined) into what may otherwise be a call-by-value language (where variables are evaluated once and the value used in every reference, a language like Qi or Racket). Either call-by-name or call-by-value languages are associative (TODO: in what sense?), but mixing them (e.g., by inlining) in some settings is non-associative. It turns out that the answer for when inlining can be done is that inlining is sound when associativity holds in the context (TODO: handwavy). Because duploids need not be associative, they provide a general foundation wherein proofs can express both associative and non-associative cases, mixing them, and establish positive and negative results.

Somewhere in all this, Eutro might also be looking into Freyd categories, which have something to do with Arrows, which apparently have a lot to do with Qi. So, these rabbit holes may well be in our future. Hopefully, we will have wrapped up some of the in-progress compiler work by then so that we can venture boldly into these design and theoretical aspects of Qi!

The Weather and Other Interesting Things

The Changing Seasons

It's been getting colder in Prague, but the temperature is still above zero.

Lately, atmospheric rivers have returned to California. This interesting (in fact Interesting) weather phenomenon occurs annually on the US West Coast, bringing large amounts of water ("as much as a river") from the Pacific in the form of rain and snow. Incidentally, every 200-400 years, such atmospheric rivers lead to catastrophic flooding, and the entire Central Valley, which looks like a bathtub in elevation maps (seriously, check it out), becomes filled with water.

On the subject of rain, Dominik mentioned that a friend of his works on technology that predicts the type and severity of rain based on the shape of drops of water!

A Real Tee Junction

This week Sid had to deal with a clogged drain in his apartment, where the bathroom sink and kitchen sink appeared to be interacting in strange ways — improving one was making the other worse! He and his partner soon realized that the two fixtures are likely connected by a tee junction somewhere behind the walls before draining into the common building drain! They managed to use a drain snake (probe debugger?), a plunger (idea for a new debugging tool?), and some elbow grease, and after much blood, sweat, and tears, the flows are now functional again without any side effects.

New Hardware

Eutro has finally set up her computer! The gloves are off and she's getting ready for some L337 hacking 😎. She started in the deep end by running a proof using Rocq which has been going for several days now. She's convinced her proof is valid and that it must terminate, but as the old saying goes, she's only proved it, not tried it.

Dominik has a new 800 GB GDDR shared soldered RAM machine running DeepSeek R1. He's suspicious of artificial intelligence, preferring to rely on natural intelligence, but with this new hardware he can at least keep his enemies close.

Comonads

Eutro has learned that a comonad is a comonoid in the category of endofunctors (what's the coproblem?). She lamented that this kind of pedagogy, while amusing, doesn't engender a sound intuition while learning about these concepts. Of course, one can unpack such definitions and understand their mechanics, but this alone isn't enough. She feels it's also important, while learning, (1) to have motivation for why the definition exists, to focus the mind on a tangible goal, (2) to bear in mind examples that the definition applies to, conveying a sense of its scope, and (3) to think about the formula in terms of its properties and develop a feel for what the formula allows you to do in the "calculus" of the specific domain, for which working through proofs can help.

Preach, Eutro! ✊😼 We nominate Eutro for Chief Monad Tutorial Writer.

She is currently going through the infamous Categories for the Working Mathematician.

CRISPR

Dominik has been working on cryptographic ways of securely slicing and manipulating genomic data. We joked that he's "going CRISPR" on the data, operating on it in the same way that CRISPR operates on the genome!

Elacarte

Sid is very close on Elacarte, the Emacs package discovery tool. But he hasn't had any time to work on it recently and it is for the moment stalled 🫤

Rhombus: the New Python?

Dominik observed that Rhombus has python-esque syntax but Chez-like performance, making it a good candidate for adoption in settings currently using Python. If we can have a good data science story for the ecosystem, perhaps with Qi + Machete, then we really might be onto something.

Scheduling

It's Thanksgiving next week in the US, so Sid may not be able to join the call for long as he will be visiting family.

The following week, Dominik won't be able to attend as he will be at a meeting of the 2600 club.

Next Steps

(Some of these are carried over from last time)

• Add bindings and effects to the Redex semantics (including: ensure that test cases validate that scoping rules are purely lexical and not dynamic)
• 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 (Nov 14), Michael (Nov 21), Sid