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 p
swap operand order — the arrow still points from FK to referenced key
JOIN f
left and right operands

Each can be a table, view, CTE, subquery, or parenthesized join. The proof checks each entire operand result, even when the named columns come from an exposed table inside it.

[join type]

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

FOR KEY left_name (…)

The first list names columns exposed by the left operand; the second names columns exposed by the right operand. Both require a qualifier: an alias, table or CTE name, or a qualified name such as sales.orders.

->

The left operand is the referencing side. The right operand supplies the referenced key: a lookup.

<-

The right operand is the referencing side. It can supply several referencing rows for each key on the left.

right_name (…)

The name must be exposed by the right operand. An alias hides the original name. Pairing is positional; both lists have the same length. The arrow contains no whitespace or comment separator.

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

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

Mathematical conditions

These conditions apply at the join point. The DBMS proves them from the referential constraint and query structure before execution.

1 Uniqueness

Uniqueness of all-non-null referenced keys.

2 Match existence

Match existence for every all-non-null referencing key.

3 Non-null or preserved

At least one of the following:

a) All referencing key values are non-null.
b) The <join type> preserves the referencing operand.

referencing keys 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 (…) -> p (…)
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 (…) <- f (…)
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. These forms do not add unmatched referenced rows.

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

The rule behind the list: the outer-preserved side, if any, must be the referencing side. Preserving the referenced side (a RIGHT … ->, LEFT … <-, or any FULL) can add unmatched referenced 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). The PostgreSQL prototype additionally proves some cases with matching direct key-equality filters on both sides
3NON-NULL OR PRESERVED referencing operand (3a) a NOT NULL constraint — or (3b) a join type that preserves the referencing side upstream outer-join null-extension removes non-null evidence; a preserving join type still satisfies condition 3b

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 · correlated subqueries · expressions over keys

Stored key joins (views, SQL-body routines) must retain a valid proof. When a constraint is dropped, the DBMS considers alternative referential constraints, non-null evidence and uniqueness proofs. Only when no valid proof remains does RESTRICT reject the drop, or CASCADE remove 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.