Type System

AXON’s type system is fundamentally different from traditional programming languages. Instead of representing memory layouts or data structures, AXON types represent epistemic states — the nature, reliability, and provenance of information.

Core Principle

Epistemic Types = Meaning TypesTypes in AXON track what information means and how reliable it is, not how many bytes it occupies in memory.

This enables the compiler and runtime to enforce semantic correctness: for example, preventing an Opinion from being used where a FactualClaim is required, or propagating Uncertainty through computations to maintain epistemic honesty.

The Partial Order Lattice

AXON’s type system is formalized as a partial order lattice (T, ≤), where ≤ represents the subsumption relationship between types.

Lattice Structure

            ⊤ (Any)
              │
    ┌─────────┼─────────────┐
    │         │             │
FactualClaim  Opinion  Speculation
    │                       │
 CitedFact            Uncertainty
    │
HighConfidenceFact
    │
    ⊥ (Never)

Subsumption Rule

Type Subsumption: If T₁ ≤ T₂, then T₁ can be used wherever T₂ is expected.

Examples:

CitedFact ≤ FactualClaim — A cited fact is a factual claim
HighConfidenceFact ≤ CitedFact — A high-confidence fact is a cited fact
Opinion ≤ Any — An opinion is some form of information
Opinion ≰ FactualClaim — An opinion cannot satisfy a factual claim requirement

Type Categories

1. Epistemic Types (Reliability)

Track the epistemic status of information — how certain, verifiable, or grounded it is.

FactualClaim

Information presented as objectively verifiable fact.

type Party {
  name: FactualClaim,
  role: FactualClaim
}

Subsumption: FactualClaim ≤ Any
Cannot contain: Opinion, Speculation

CitedFact

A factual claim with explicit source attribution.

anchor RequiresCitation {
  require: CitedFact
  on_violation: raise AnchorBreachError
}

Subsumption: CitedFact ≤ FactualClaim ≤ Any

HighConfidenceFact

A cited fact with confidence score ≥ 0.85 (configurable).Subsumption: HighConfidenceFact ≤ CitedFact ≤ FactualClaim ≤ Any
Use case: Medical, legal, or financial domains requiring high certainty.

Opinion

Subjective judgment or interpretation.

type Risk {
  score: RiskScore,          // objective
  mitigation: Opinion?       // subjective
}

Critical: Opinion ≰ FactualClaim — opinions never satisfy factual requirements.

Uncertainty

Lack of sufficient information to make a determination.

Taint Propagation: Any computation involving Uncertainty produces Uncertainty. This is enforced at compile time.

let fact: FactualClaim = "The contract was signed in 2020"
let unknown: Uncertainty = recall("signer_address")
let result = weave [fact, unknown]  // result: Uncertainty

Speculation

Conjecture without evidence.

anchor AgnosticFallback {
  forbid: Speculation
  on_detection: raise AnchorBreachError
}

Subsumption: Speculation ≤ Any but incompatible with most epistemic types.

2. Content Types (Data)

Represent structured or unstructured information that flows through pipelines.

Type	Description	Example Use
`Document`	Raw text document	Contract PDFs, emails
`Chunk`	Segmented portion of a document	Paragraph, section
`EntityMap`	Extracted structured entities	Parties, dates, obligations
`Summary`	Condensed representation	Executive summary
`Translation`	Language-translated content	EN → ES

Example: Content pipeline

flow ProcessDocument(doc: Document) -> Summary {
  step Segment {
    given: doc
    ask: "Split into logical sections"
    output: List<Chunk>
  }
  
  step Extract {
    probe Segment.output for [entities, dates, amounts]
    output: EntityMap
  }
  
  step Summarize {
    given: Extract.output
    ask: "Generate executive summary"
    output: Summary
  }
}

3. Analysis Types (Metrics)

Quantitative or qualitative assessments with bounded ranges.

type RiskScore(0.0..1.0)

type Risk {
  score: RiskScore,
  description: FactualClaim
}

Range Constraints: Analysis types have built-in validation. Values outside the declared range raise ValidationError.

4. Structural Types (User-Defined)

Custom types for domain-specific entities.

contract_analyzer.axon

type Party {
  name: FactualClaim,
  role: FactualClaim
}

type Risk {
  score: RiskScore,
  mitigation: Opinion?
}

type ContractAnalysis {
  parties: List<Party>,
  obligations: List<FactualClaim>,
  risks: List<Risk>,
  overall_confidence: ConfidenceScore
}

Compositional Types: User types can embed epistemic types, enforcing semantic constraints at every level.

Type Checking

AXON performs semantic type checking at compile time via the TypeChecker module.

Compatibility Matrix

The type checker uses an EpistemicLattice class to determine type compatibility:

type_checker.py

class EpistemicLattice:
    """Partial Order Lattice for AXON epistemic types."""
    
    _parents = {
        "HighConfidenceFact": "CitedFact",
        "CitedFact": "FactualClaim",
        "FactualClaim": "Any",
        "Opinion": "Any",
        "Speculation": "Any",
        "Uncertainty": "Any",
        "Any": None,
        "Never": None,
    }
    
    @classmethod
    def subsumes(cls, subtype: str, supertype: str) -> bool:
        """Check if subtype ≤ supertype in the lattice."""
        # Walk up the parent chain
        current = subtype
        while current is not None:
            if current == supertype:
                return True
            current = cls._parents.get(current)
        return False

Validation Rules

Assignment Compatibility

Can source_type be assigned to target_type?

let claim: FactualClaim = get_cited_fact()  // ✅ CitedFact ≤ FactualClaim
let claim: FactualClaim = get_opinion()     // ❌ Opinion ≰ FactualClaim

Parameter Passing

Can argument_type satisfy parameter_type?

flow Verify(input: FactualClaim) -> Boolean { ... }

run Verify(cited_fact)   // ✅
run Verify(opinion)      // ❌ Type error

Return Type Checking

Does step output match declared type?

step Extract {
  ask: "What is the contract date?"
  output: FactualClaim  // Checked at runtime
}

Uncertainty Propagation

Any operation on Uncertainty yields Uncertainty.

let a: FactualClaim = "Known fact"
let b: Uncertainty = recall("unknown_key")
let c = weave [a, b]  // c: Uncertainty (taint)

Runtime Validation

While the TypeChecker catches structural issues at compile time, semantic validation happens at runtime via the SemanticValidator.

How It Works

Step Execution — Model produces output
Semantic Classification — Runtime determines epistemic type
Lattice Check — Validator checks actual_type ≤ declared_type
Action — Pass, raise ValidationError, or trigger refine

semantic_validator.py

def validate_output(actual: Any, expected_type: str) -> bool:
    """Validate that actual output matches expected epistemic type."""
    actual_type = classify_epistemic_type(actual)
    if not EpistemicLattice.subsumes(actual_type, expected_type):
        raise ValidationError(
            f"Type mismatch: expected {expected_type}, got {actual_type}"
        )
    return True

ValidationError (Level 1): Raised when output type doesn’t match declaration. Can trigger automatic refinement if configured.

Special Type Rules

Optional Types

Use ? suffix for optional fields:

type Risk {
  score: RiskScore,
  mitigation: Opinion?   // May be absent
}

List Types

type ContractAnalysis {
  parties: List<Party>,
  risks: List<Risk>
}

Range Types

type RiskScore(0.0..1.0)     // Compile-time range constraint
type AgeInYears(0..150)       // Integer range

Union Types (Planned)

type Outcome = Success | Failure | Pending  // Coming in Phase 5

Type Inference

AXON performs limited type inference for intermediate values:

step Extract {
  given: doc                  // Type inferred from doc: Document
  ask: "Extract entities"
  output: EntityMap           // Explicit declaration required
}

step Assess {
  given: Extract.output       // Type inferred as EntityMap
  ask: "Assess risks"
  output: RiskAnalysis
}

Design Choice: Step outputs require explicit type declarations for clarity and safety. Intermediate expressions support inference.

Comparison with Other Type Systems

Feature	TypeScript	Python	Haskell	AXON
Structural types	✅	❌	❌	✅
Epistemic types	❌	❌	❌	✅
Runtime validation	❌	Partial	❌	✅
Uncertainty propagation	❌	❌	❌	✅
Semantic subsumption	❌	❌	Partial	✅

Next Steps

Cognitive Primitives

Learn about the 12 core primitives

Error Handling

See how type errors are handled

Compilation Pipeline

Understand type checking in the compiler

Examples

See types in real programs

Get Started

Core Concepts

Language Reference

Examples

Type System

Core Principle

The Partial Order Lattice

Lattice Structure

Subsumption Rule

Type Categories

1. Epistemic Types (Reliability)

2. Content Types (Data)

3. Analysis Types (Metrics)

4. Structural Types (User-Defined)

Type Checking

Compatibility Matrix

Validation Rules

Runtime Validation

How It Works

Special Type Rules

Optional Types

List Types

Range Types

Union Types (Planned)

Type Inference

Comparison with Other Type Systems

Next Steps

Cognitive Primitives

Error Handling

Compilation Pipeline

Examples

Build docs developers (and LLMs) love

Get Started

Core Concepts

Language Reference

Examples

​Core Principle

​The Partial Order Lattice

​Lattice Structure

​Subsumption Rule

​Type Categories

​1. Epistemic Types (Reliability)

​2. Content Types (Data)

​3. Analysis Types (Metrics)

​4. Structural Types (User-Defined)

​Type Checking

​Compatibility Matrix

​Validation Rules

​Runtime Validation

​How It Works

​Special Type Rules

​Optional Types

​List Types

​Range Types

​Union Types (Planned)

​Type Inference

​Comparison with Other Type Systems

​Next Steps

Cognitive Primitives

Error Handling

Compilation Pipeline

Examples

Build docs developers (and LLMs) love

Core Principle

The Partial Order Lattice

Lattice Structure

Subsumption Rule

Type Categories

1. Epistemic Types (Reliability)

2. Content Types (Data)

3. Analysis Types (Metrics)

4. Structural Types (User-Defined)

Type Checking

Compatibility Matrix

Validation Rules

Runtime Validation

How It Works

Special Type Rules

Optional Types

List Types

Range Types

Union Types (Planned)

Type Inference

Comparison with Other Type Systems

Next Steps