Skip to content

Theoretical Foundations

This page covers the formal type-theoretic framework underlying ContextFS and type-safe context engineering.

Formal Framework

Definitions

Definition: Context Type

A context type $\Gamma$ is a specification that constrains the space of valid responses. Formally, $\Gamma$ defines a set of constraints ${c_1, c_2, ..., c_n}$ that any valid response must satisfy.

Definition: Response Term

A response term $t$ is a model output. We write $t : \Gamma$ to indicate that $t$ satisfies all constraints in $\Gamma$.

Definition: Type Safety

A context $\Gamma$ is type-safe if there exists a unique equivalence class of responses $[t]$ such that for all valid responses $t_1, t_2 : \Gamma$, we have $t_1 \sim t_2$ under semantic equivalence.

The Typing Judgment

We define a typing judgment for context engineering:

$$ \Gamma \vdash t : T $$

Read as: "Under context $\Gamma$, response $t$ has type $T$."

Type Constructors

Building complex types from simpler ones:

Constructor Meaning Example
$A \times B$ Product (and) JSON with fields A and B
$A + B$ Sum (or) Either format A or B
$A \to B$ Function Given input A, produce B
$\Pi_{x:A} B(x)$ Dependent Output type depends on input

Dependent Types in Context

The most powerful aspect: response types can depend on context values.

# Type depends on the code being reviewed
def review_type(code: str) -> Type[Review]:
    if "async" in code:
        return AsyncCodeReview  # Includes concurrency checks
    else:
        return SyncCodeReview   # Standard checks

Formally:

$$ \Pi_{\text{code} : \text{String}} \text{ReviewType}(\text{code}) $$

The Correspondence

Programming Languages Context Engineering
Source code Context (prompt + examples)
Type specification Output schema
Compilation Inference
Type error Invalid response
Type inference Understanding implicit constraints
Subtyping Response satisfies stricter constraints

Proof-Theoretic View

Under Curry-Howard correspondence:

  • Types = Propositions
  • Terms = Proofs
  • Type inhabitation = Provability

Context engineering becomes proof search:

Given context $\Gamma$ (propositions/assumptions), find response $t$ (proof) such that $t : T$ (proof of proposition $T$).

Why AlphaFold Succeeds

Protein folding is proof search where:

  • Sequence = Type constraints
  • Structure = Proof term
  • Anfinsen's dogma = Type safety guarantee

AlphaFold learned efficient proof search heuristics for a well-typed problem.

Failure Modes as Type Errors

Underdetermined Types

$$ \Gamma \vdash t_1 : T \quad \Gamma \vdash t_2 : T \quad t_1 \not\sim t_2 $$

Multiple non-equivalent valid responses exist.

Example: 

Context: "Write a function"
Valid responses: Any function in any language

Overdetermined Types (Uninhabited)

$$ \nexists t. \; \Gamma \vdash t : T $$

No valid response can satisfy all constraints.

Example: 

Context: "Write a 10-word essay covering all of machine learning in depth"

Type Mismatch

$$ \Gamma \vdash t : T' \quad T' \not<: T $$

Response satisfies a different type than expected.

Example: 

Expected: JSON object
Got: Markdown text

Chaperone Systems

Inspired by molecular chaperones that guide protein folding:

Retry Chaperone

def retry_chaperone(prompt, target_type, max_attempts=3):
    for attempt in range(max_attempts):
        response = model.generate(prompt)
        try:
            return target_type.model_validate_json(response)
        except ValidationError as e:
            prompt = f"{prompt}\n\nPrevious attempt failed: {e}\nTry again:"
    raise TypingError("Could not inhabit type")

Progressive Refinement Chaperone

def progressive_chaperone(task, target_type):
    # Start with broad type
    outline = model.generate(f"Outline: {task}")

    # Refine to specific type
    details = model.generate(
        f"Given outline:\n{outline}\n\nNow provide: {target_type.schema()}"
    )

    return target_type.model_validate_json(details)

Ensemble Chaperone

def ensemble_chaperone(prompt, target_type, n=3):
    responses = [model.generate(prompt) for _ in range(n)]
    validated = [target_type.model_validate_json(r) for r in responses]
    return consensus(validated)  # Aggregate consistent responses

Implications for AI Safety

Alignment as Type Safety

If we could specify human values as a type $V$, alignment becomes:

$$ \forall \text{action} \; a. \; \Gamma_{\text{values}} \vdash a : V $$

All actions must inhabit the "aligned" type.

Robustness as Type Preservation

System is robust if type safety holds under perturbation:

$$ \Gamma \vdash t : T \implies \Gamma' \vdash t' : T \quad \text{for small } \delta(\Gamma, \Gamma') $$

Interpretability as Type Inference

Understanding a model's behavior = inferring what type constraints it has learned:

$$ \text{Given outputs } t_1, t_2, ..., t_n \text{, infer } \Gamma \text{ such that } \Gamma \vdash t_i : T $$

Practical Applications

1. Prompt Engineering Guidelines

From type theory:

  • Be explicit: Specify output types precisely
  • Be complete: Ensure constraints determine unique response class
  • Be consistent: Avoid contradictory constraints

2. Evaluation Metrics

  • Type inhabitation rate: % of responses that validate against schema
  • Semantic consistency: Agreement between responses to same prompt
  • Constraint satisfaction: % of explicit constraints met

3. System Design

  • Use Pydantic/JSON Schema for explicit typing
  • Implement chaperone patterns for reliability
  • Design for progressive type refinement

References

  1. Anfinsen, C. B. (1973). Principles that govern the folding of protein chains. Science.

  2. Jumper, J., et al. (2021). Highly accurate protein structure prediction with AlphaFold. Nature.

  3. Wadler, P. (2015). Propositions as Types. Communications of the ACM.

  4. Martin-Löf, P. (1984). Intuitionistic Type Theory.

  5. Long, M. & YonedaAI Collaboration. (2025). Type-Safe Context Engineering. Preprint.