Channels and Polarity

definition design

Reconciling AutoBayes’ $(X,[[c]],Y)$ with ImplicitREDDiff’s $P_{in}+P_{out}+P_{latent}=\mathrm{Id}$.

Sources: original to this vault (design and analysis; no single paper).

Theory (CT-ML wiki): Compact Closed Category · Bayesian Inversion · Open Model · Lens

The two trichotomies

AutoBayes (Definition 1) gives every model three spaces:

$c:X⇝[[c]]\times Y$

	AutoBayes name	role
$X$	unobserved	inferred; the posterior is over this
$Y$	observed	clamped to data
$[[c]]$	latent	internal scratch, revealed or marginalised

ImplicitREDDiff gives every factor three diagonal selection matrices with $P_{in}+P_{out}+P_{latent}=\mathrm{Id}$ and pairwise-zero products, assembling a precision-weighted projector

$P={\rho }_{in}{P}_{in}+{\rho }_{out}{P}_{out}+{\rho }_{latent}{P}_{latent}$

The names cross over — read this twice

AutoBayes’ unobserved $X$ is the thing you solve for, i.e. the note’s output $P_{out}$. AutoBayes’ observed $Y$ is the thing you clamp, i.e. the input $P_{in}$.

$X⟷P_{out},Y⟷P_{in},[[c]]⟷P_{latent}$

The inversion $c_{\pi }^{\prime }:Y⇝X\times [[c]]$ runs input → output in the note’s sense. The forward kernel $c$ runs the other way. The mismatch is real, not a typo in either source: “observed” is a statistical word about data availability, “input” is an operational word about evaluation order, and in Bayesian inference those point in opposite directions.

Notation used in this vault

The rest of the vault uses one convention, the machine-learning one, because it is what most readers bring:

$$Z=X\times Y\times U,z=(x,y,u),$$

symbol	role	polarity	selection	AutoBayes
$Z$, $z$	the joint space of a factor, a point of it		$\mathrm{Id}$	—
$X$, $x$	inputs: clamped to evidence	Observed()	$P_{in}$	$Y$
$Y$, $y$	outputs: solved for	Unobserved()	$P_{out}$	$X$
$U$, $u$	latents: internal	Latent()	$P_{latent}$	$\llbracket c
rbracket$
$z_0$	the evidence: clamp values on $X$, anchors elsewhere
$
ho$	per-coordinate precision; $\infty$ = hard clamp, $0$ = free		$P=\mathrm{diag}(\rho )$

So our $X$ is AutoBayes’ $Y$ and our $Y$ is AutoBayes’ $X$. Notes that quote AutoBayes definitions use its letters and say so; everywhere else the table above holds. Papers with their own letters (RED-Diff’s $x_0$ and $y$, ProxDM’s $x$) get a one-line notice in the note that discusses them, and are then translated. Where a family has an entrenched name for the joint state, such as the DEQ’s hidden state $z^{\ast }$, it is the latent $u$ of this table when the DEQ is read as a relation.

Once that is said, the correspondence is exact, and $\rho$ has a clean reading: the precision with which each block is clamped. ${\rho }_{in}\to \infty$ is a hard clamp (a cup); ${\rho }_{out}=0$ leaves the block free.

Why polarity must be dynamic

A Lux layer has a fixed direction. A Lenticulum factor is a relation $R_{\theta }\subseteq X_1\times \cdots \times X_n$ and has none: the same factor $x^2+y^2=1$ can be asked for $y$ given $x$, or $x$ given $y$, or neither given nothing.

Categorically this is compact closure: the cup and cap let you bend any leg from unobserved to observed and back. Operationally it means a factor’s get/put pair does not exist until you choose. Hence:

Factor  +  Polarity  ──►  parametric lens  ──►  message

The data type

A channel is a named port of a factor with a space attached. A polarity is an assignment of one of three states to each channel:

abstract type ChannelPolarity end
struct Observed  <: ChannelPolarity end   # input  X (AutoBayes Y)   / P_in     / clamped to data
struct Unobserved<: ChannelPolarity end   # output Y (AutoBayes X)   / P_out    / inferred, posterior over it
struct Latent    <: ChannelPolarity end   # latent U (AutoBayes ⟦c⟧) / P_latent / internal, marginal or revealed

with Polarity a NamedTuple{names} of these. The type-level names means a polarised factor’s lens type is known at compile time and Julia can specialise the assembled kernel — this is the payoff for putting the polarity in the type domain rather than a runtime Dict.

Legality

Not every polarity is legal for every factor. A Gaussian(μ, σ) factor can be inverted for μ given x and σ, but a factor whose forward kernel is a one-way hash cannot be inverted at all. So a factor declares which polarities it supports:

supports_polarity(factor, pol)::Bool

and a graph compiles only if every scheduled message uses a supported polarity. The DAG restriction of Lux is replaced by a polarity-legality check. That is the concrete form the README’s “arbitrary connected graph” claim takes in the type system.

The three ways a polarity can be realised

how the factor answers a polarity	model family	cost
closed form (conjugate, invertible map)	Gaussian/linear, normalising flows	cheap
root-finding on a residual $r_{\theta }(x)=0$	algebraic varieties, DEQ, NeuralODE	Newton/fixed point
proximal step on an energy	diffusion / RED-Diff	iterative denoising

These are exactly the three families of Implicit Learners. Which one is available is a property of the factor; the graph does not need to know, which is the point of the abstraction.

Polarities are Prolog's modes, and Mercury checks them statically

A logic-programming predicate has no fixed direction either, and which arguments are bound at the call site is its mode. Mercury is Prolog with a statically-verified mode and determinism system — the precedent for making supports_polarity decided rather than declared. See Prolog and Logic Programming §2.

Related: Prolog and Logic Programming, Open Models and Latent Channels, Open Models and Latent Channels, Implicit Learners, ImplicitREDDiff, channels, The Table Revisited, Geometric Deep Learning and Physical Laws