SHAPE

SHIFT

Back to homepage

Semantics Are Constraints, Not A Tree

It is tempting to imagine a universal semantic representation as one enormous tree.

Parse every language, normalize the nodes, and then merge the tree.

That sounds clean, but it collapses too much.

Languages do not only differ in syntax. They differ in what they force you to prove. One language makes ownership explicit. Another makes effects implicit. One has structural interfaces. Another has nominal traits and coherence rules. One has pattern matching with exhaustiveness. Another has a switch statement with fallthrough.

The useful universal layer is not a perfect tree.

It is a set of constraints.

The interlingua is stronger when it keeps source text, identity, type, effect, ownership, protocol, runtime, and proof layers separate.

The Tree Is Too Flat

A tree is good for containment.

file
  module
    declaration
      expression
        identifier

Containment matters. Source spans, comments, imports, declarations, and generated output all need positions.

But most merge questions are not containment questions.

They are questions like:

does this borrow still end before mutation?
does this interface still satisfy the protocol?
does this match still cover every variant?
does this selector still reach the same rendered target?
does this async operation still happen in the same order?
does this public type still assign to the old contract?

Those are constraint questions.

If the representation only says where a node lives, the coordinator still has to infer what the node means. That is where unsafe merges hide.

Constraint Families

A better semantic record is made of many small families.

Constraint MatrixDifferent Surfaces Need Different Proof
SurfaceClaimRequired proofCurrent evidenceRoute
RequiredTypePublic shape survivedDeclaration, assignability, or type oracleFields, generics, overloads, aliasesGate public API
MissingOwnershipMutation rights are preservedBorrow and move constraintsLoan scope, alias mode, escape boundaryRequire proof
RequiredProtocolContract obligations survivedRequirement and implementation evidenceMethods, associated types, dispatch, coherenceReview target contract
MissingPatternVariant dispatch stayed totalExhaustiveness and guard evidenceCases, payloads, default, fallthroughProve coverage
MissingRuntimeOutput behaves under declared conditionsRuntime probe capsuleTrace, DOM, layout, effects, accessibilityRun bounded proof
A semantic system should keep proof obligations separate. Green type evidence should not accidentally imply runtime, ownership, or pattern evidence.

The important part is not the number of families.

The important part is that each family can fail independently.

A target may preserve the type shape but lose ownership semantics.

A target may preserve an interface but lose dispatch behavior.

A target may preserve the variants but lose exhaustiveness because a default branch swallowed the missing case.

Those distinctions are what make review smaller.

Merge As Constraint Admission

A semantic merge is not “understand the program, then apply.”

It is closer to:

lift source into records
compare changed identities
collect constraints
ask what proof each constraint requires
route the candidate
admit only the claims that are proved
Constraint RecordReviewable
One Candidate, Several Obligations
Candidate
Translate Result<T, E> into a tagged objectThe output can look simple while the proof surface is not.
Type
Ok and Err payloads representedThe target object shape carries both variant payloads.
Pattern
Every source match arm has a target branchExhaustiveness and default behavior are separate claims.
Runtime
No broad behavior claimThe record can be useful without claiming total equivalence.
Route
Admit type shape, request pattern proofPartial proof produces narrower follow-up work.
A constraint record lets the system admit what is actually proved and route what is still missing.

This turns “semantic understanding” into an inspectable object.

The coordinator does not need to believe a worker’s summary. It can inspect which constraint families are present, which are missing, and which claims are explicitly false.

Missing Constraints Are Useful

A missing constraint is not just a failure.

It is a better task.

  1. Tree nodeweak
    Can proveA construct exists at a span.
    Stops atDoes not prove the construct keeps its meaning.
    Attach source binding
  2. Identitybound
    Can proveThe same region can be followed across edits.
    Stops atDoes not prove the region is safe to merge.
    Compare changed regions
  3. Constrainttyped
    Can proveA specific semantic obligation is known.
    Stops atDoes not prove the obligation is satisfied.
    Ask for family proof
  4. Proofbounded
    Can proveThe obligation is satisfied under declared evidence.
    Stops atDoes not imply unrelated constraints.
    Admit scoped claim
  5. Decisionaccepted
    Can proveThe candidate may cross the named boundary.
    Stops atDoes not erase future stale checks.
    Apply or rebase
The ladder from syntax to admission is a ladder of stronger constraints, not a single jump from parse tree to merge.

If ownership proof is missing, ask for ownership proof.

If protocol coherence is missing, ask for protocol evidence.

If runtime order is missing, run a runtime probe.

If pattern exhaustiveness is missing, create a focused coverage fixture.

That is the practical reason to model semantics as constraints. The system can produce the next correct unit of work.

The Mental Model

A universal semantic layer should not try to erase the differences between languages.

It should preserve those differences as named constraints.

The tree says where meaning lives.

The constraints say what must stay true.

The merge decision should be based on the constraints, not on a vague claim that the tree looks reasonable.