A foreign-key-aware join, proven at compile time

Key Joins in a Nutshell

A third join specification besides ON and USING. FOR KEY declares that an equijoin follows a foreign key. The DBMS proves — at compile time, against the intermediate result at the join point — that every referencing row survives exactly once, enriched with its unique referenced row. What cannot be proven does not compile: the rules are sound, not complete.

1 · The two arrow forms

One construct, written either direction

The arrow encodes the foreign key. Flip it and the two roles swap places — but the shape of the statement stays the same. Hover or tap any highlighted token to see what it does.

JOIN f
flip the arrow — the roles swap places, the shape doesn't
JOIN p
<left operand>

The query built so far — table, view, CTE, subquery, or join tree. The proof runs against this intermediate result, not the base tables.

[join type]

[INNER] / LEFT / RIGHT / FULL — orthogonal to FOR KEY. Outer types only change null-extension of unmatched rows. CROSS and NATURAL: excluded.

FOR KEY (…)

Declares that this equijoin follows a FOREIGN KEY; the compiler must prove it or the statement fails (see the errors). The list is always columns of the newly joined relation — never alias-qualified. Both lists: equal arity, pairwise comparable types.

->

The newly joined relation is the referencing side: descend to detail — the only join where rows can multiply (result shape).

<-

The newly joined relation is the referenced side: a pure lookup — the running row count is unchanged (result shape).

… after the arrow

An alias already visible in the left operand, and its columns. Pairing is positional — 1st with 1st, …, nth with nth; order need not match the constraint declaration.

[FILTER (WHERE pred)]

Optional, join-local: ANDed into the match condition. Applied after the proof — never proof evidence for this join.

2 · What both forms mean

An ordinary equijoin — plus a proof obligation

Either arrow desugars to the same plain equijoin and the same output columns as ON. The one thing it adds is a compile-time proof that ON can never give you.

Both forms mean
… JOIN … ON f.f1 = p.p1 AND … AND f.fn = p.pn [AND pred]

Output columns are exactly as with ON — no USING-style column merging.

Required declaration
FOREIGN KEY (f1, …, fn) REFERENCES p (p1, …, pn)

On f's base table, ENFORCED and NOT DEFERRABLE — plus the proof facts still alive at the join point.

The desugared join is what runs. The FOR KEY wrapper adds nothing at runtime — its entire job is the compile-time proof that this equijoin really follows the declared key and preserves the referencing rows.

3 · The contract

A key join holds iff three conditions do

State it over two multisets: the referencing multiset (the referencing side projected onto its key columns) and the referenced multiset (the referenced side projected onto its key columns, all-non-NULL rows only).

1 Uniqueness

Every tuple of the referenced multiset occurs exactly once — so no referencing row can match more than one, and none is duplicated.

2 Containment

Every all-non-NULL tuple of the referencing multiset appears among the referenced tuples — so no referencing row is dropped for want of a match.

3 Null safety

A referencing tuple with a NULL component matches nothing. Either (3a) every f-column is proven NOT NULL, or (3b) the join type preserves the referencing side.

referencing multiset referenced — each ×1 NULL ×1 ×1 ×1 ×1 ×1
GUARANTEE

Every referencing row appears exactly once in the result; each all-non-NULL key is enriched with its unique referenced row.

4 · Result shape

The arrow direction decides which side sets the rows

The diagrams follow the same visual convention as the contract: colored cells mark key values, grey cells represent other columns, and arrows point from referencing keys to referenced keys.

… LEFT [OUTER] JOIN p FOR KEY (…) <- f (…)
LEFT OUTER lookup result shape Referencing rows are on the left, referenced rows are on the right, and the joined result keeps the referencing row count. LEFT OPERAND — REFERENCING NEW RELATION — REFERENCED NULL ×1 ×1 ×1 ×1 ×1 RESULT NULLNULL
… RIGHT [OUTER] JOIN f FOR KEY (…) -> p (…)
RIGHT OUTER descend result shape Referenced rows are on the left, referencing rows are on the right, and the joined result keeps each new referencing row exactly once. LEFT OPERAND — REFERENCED NEW RELATION — REFERENCING ×1 ×1 ×1 ×1 ×1 NULL RESULT NULLNULL

5 · Cardinality-preserving forms

Four forms keep the result 1 : 1 with the referencing side

Result rows = referencing rows, each exactly once, nothing else. These are exactly the join types that never null-extend the referenced side.

Guaranteed 1 : 1 with the referencing side
…       [INNER] JOIN f FOR KEY (…) -> p (…)
… RIGHT [OUTER] JOIN f FOR KEY (…) -> p (…)
…       [INNER] JOIN p FOR KEY (…) <- f (…)
…  LEFT [OUTER] JOIN p FOR KEY (…) <- f (…)

The rule behind the list: the outer-preserved side, if any, must be the referencing side. Null-extending the referenced side (a LEFT … ->, RIGHT … <-, or any FULL) would add its unmatched rows and break the 1 : 1.

Visual scan rule: in a FROM clause made only of Key Joins, if every FOR KEY arrow points <- and every join is INNER or LEFT, the first FROM relation is preserved 1 : 1.

6 · The compile-time proof

Declarations grant facts; query shape revokes them

Each condition becomes a fact the compiler must still hold at the join point. Schema declarations grant the facts; upstream query operations can take them away.

Fact needed at the join point Granted by ✓ Revoked by ✗
1UNIQUE on (p1, …, pn) of the referenced side PRIMARY KEY or UNIQUE — ENFORCED, NOT DEFERRABLE; or, mid-query, GROUP BY / DISTINCT on exactly the key columns a preceding join that can duplicate the referenced side
2COVERAGE — every all-non-NULL (f1, …, fn) tuple has its referenced row FOREIGN KEY — ENFORCED, NOT DEFERRABLE filtering the referenced side (WHERE, HAVING, sampling, set ops, OFFSET / FETCH) — unless each direct key-equality filter is matched on the referencing columns
3NOT NULL on f1 … fn of the referencing side (3a) a NOT NULL constraint — or (3b) a join type that preserves the referencing side upstream outer-join null-extension

Propagation through derived tables

base tables

declarations grant the facts: PRIMARY KEY / UNIQUE · FOREIGN KEY · NOT NULL

FACTS FLOW→
view · CTE · subquery

facts pass through while every named column traces to exactly one base column

→
opaque — no facts

set ops · recursive CTEs · LATERAL · expressions over keys

Stored key joins (views, SQL-body routines) depend on every proof source. Dropping or weakening one is RESTRICTed, or CASCADE drops the dependent definition.

7 · When it won't compile

Four ways the proof can fail

If no proof can be formed, the statement is rejected before it runs. Each error maps back to the condition it couldn't establish.

E0
no matching foreign key constraint for f (f1, …, fn) referencing p (p1, …, pn)

The named column pairing must match a declared referential constraint.

E1
1 referenced columns p (p1, …, pn) are not proven unique at the join point

A preceding join may duplicate the referenced side, so it is no longer unique at this point.

E2
2 not every f (f1, …, fn) value can be proven to have a matching p row

The referenced side is filtered before this key join — row coverage is lost.

E3
3 this inner join could drop referencing rows: f (f1, …, fn) can be NULL

Declared nullable, or null-extended by a preceding outer join — preserve it with an outer join type.