Types - AXON

Overview

AXON’s type system is epistemic—it tracks the nature and reliability of information, not memory layout. The type system has four layers, from simple nominal types to dependent types, all designed to remain decidable at compile-time.

Key Principle

────────── COMPILE-TIME ↑ ────────── (Types: decidable)
────────── RUNTIME ↓ ─────────────── (Contracts: verifiable)

Types never depend on LLM outputs. This ensures type checking is always decidable.

Type Layers

AXON has four type system layers:

Nominal — Name-based identity
Structural Epistemic — Cognitive compatibility
Refinement — Predicate-constrained types
Dependent (Light) — Statically parameterized types

Layer 1: Nominal Types

Nominal types are identified by name. Two types are equal only if they have the same name.

Syntax

type <Name>
type <Name> { <field>: <Type>, ... }

Examples

// Simple nominal types
type Customer
type Order
type Invoice

// Structured nominal types
type Party {
  name: FactualClaim,
  role: FactualClaim
}

type Witness {
  name: FactualClaim,
  role: FactualClaim
}

Important: Party ≠ Witness even though they have identical structure. Nominal typing uses name identity.

When to Use

Domain-specific entities
Business concepts
When structural similarity doesn’t imply semantic equivalence

Layer 2: Structural Epistemic Types

Structural compatibility based on cognitive status, not field matching.

Built-in Epistemic Types

// Epistemic types
FactualClaim      // Verifiable facts
CitedFact         // Facts with citations
Opinion           // Subjective opinions
Speculation       // Speculative statements
Uncertainty       // Uncertain information

// Content types
Document
Chunk
EntityMap
Summary
Translation

// Analysis types
RiskScore
ConfidenceScore
SentimentScore
ReasoningChain
Contradiction

Compatibility Rules

// ✅ Compatible (can substitute)
FactualClaim  <:  String
CitedFact     <:  FactualClaim
RiskScore     <:  Float

// ❌ Incompatible (NEVER substitute)
Opinion       <:  FactualClaim   // ❌ Prevented at compile-time
Speculation   <:  FactualClaim   // ❌ Prevented at compile-time
Float         <:  RiskScore      // ❌ Prevented at compile-time

// ⚠️ Uncertainty taints everything
Uncertainty   <:  ∀T             // Compatible but propagates

Example

type Risk {
  score: RiskScore,        // RiskScore is compatible with Float
  description: FactualClaim,  // Must be factual, not Opinion
  mitigation: Opinion?      // Opinion allowed here (optional)
}

flow Analyze(input: Document) -> Risk {
  step Assess {
    ask: "Calculate risk score"
    output: RiskScore  // Can use where Float is expected
  }
}

Uncertainty Propagation

Uncertainty is infectious—once data becomes uncertain, everything computed from it is also uncertain:

// If x is Uncertainty
// Then f(x) is also Uncertainty

step ProcessUncertain {
  given: uncertainData  // Type: Uncertainty
  ask: "Analyze this"
  output: Analysis      // Automatically becomes Uncertainty
}

This prevents laundering unreliable information into reliable conclusions.

Layer 3: Refinement Types

Refine base types with decidable predicates.

Range Constraints

type RiskScore(0.0..1.0)
type ConfidenceScore(0.0..1.0)
type SentimentScore(-1.0..1.0)

type Percentage(0.0..100.0)
type Rating(1.0..5.0)

Where Clauses

type HighConfidenceClaim where confidence >= 0.85

type NonEmptyList where length > 0

type ValidParty where name ≠ ∅ ∧ role ∈ ValidRoles

type AdultAge where value >= 18

Allowed Predicates

Refinement predicates must be decidable:

✅ Allowed	Example	Why
Numeric comparison	`value >= 0.95`	Computable
Emptiness check	`name ≠ ∅`	Computable
Length check	`length > 0`	Computable
Set membership	`role ∈ ValidRoles`	Finite set
Conjunction	`P ∧ Q`	Both decidable

❌ Prohibited	Example	Why
LLM judgment	`is_factual(text)`	Non-deterministic
Inference	`sentiment(x) > 0`	Requires LLM
Unbounded quantification	`∀ field: P(field)`	Undecidable

Example

type ValidRiskScore(0.0..1.0) where confidence >= 0.8

type SafeParty {
  name: FactualClaim,
  verified: Boolean
} where verified == true

flow ProcessRisk(score: ValidRiskScore) -> Report {
  // score is guaranteed to be in [0.0, 1.0] with confidence ≥ 0.8
}

Layer 4: Dependent Types (Light)

Status: Planned for v1.5+ Dependent types parameterized by static constants (not runtime values).

Planned Syntax

// Parameterized by constant
type BoundedList<T, max: 50>

type ConversationWindow<turns: 10>

// Memory with static bound
Memory<ConversationHistory[n]> where n ≤ 50

// Flow with bounded iterations
flow Refine<max_attempts: 3>(input: Draft) -> Final

What’s Allowed

✅ Allowed	Example
Integer constants	`BoundedList<Party, 100>`
Enum values	`Memory<scope: persistent>`
Arithmetic on constants	`Window<n * 2>` where `n` is const
Static bounds	`where n ≤ 50`

❌ Prohibited	Example	Why
LLM outputs	`Result<confidence: llm.score>`	Non-deterministic
Runtime variables	`List<T, len: user_input>`	Unknown at compile-time
Unbounded recursion	`Tree<depth: depth(x)>`	Undecidable

Type Definition Syntax

Simple Type

type CustomerID
type OrderID

Structured Type

type Address {
  street: String,
  city: String,
  zipcode: String
}

Range-Constrained Type

type Score(0.0..100.0)

Refined Type

type HighScore(0.0..100.0) where value >= 80.0

Type with Where Clause

type ValidEmail where matches(pattern: email_regex)

Combining Features

type ValidatedRisk(0.0..1.0) {
  score: Float,
  confidence: Float,
  source: CitedFact
} where confidence >= 0.85 ∧ source ≠ ∅

Type Expressions

Basic Type Reference

flow Process(input: Document) -> Report

Generic Types

type Result {
  items: List<Party>,
  metadata: Map<String, String>
}

Optional Types

type Risk {
  score: RiskScore,
  mitigation: Opinion?      // Optional field
}

Nested Types

type Contract {
  parties: List<Party>,
  terms: List<Term>,
  risks: List<Risk>?
}

Generic Type Parameters

Current support:

List<T>           // List of type T
List<Party>       // List of Party
List<String>      // List of strings

Optional Fields

Mark fields as optional with ?:

type Party {
  name: FactualClaim,        // Required
  role: FactualClaim,        // Required
  contact: String?           // Optional
}

Built-in Types

Primitive Types

String
Integer
Float
Boolean
Duration

Epistemic Types

FactualClaim      // Verifiable facts
CitedFact         // Facts with citations
Opinion           // Subjective opinions
Speculation       // Speculative statements
Uncertainty       // Uncertain information

Content Types

Document
Chunk
EntityMap
Summary
Translation

Analysis Types

RiskScore         // Risk assessment (0.0-1.0)
ConfidenceScore   // Confidence level (0.0-1.0)
SentimentScore    // Sentiment (-1.0-1.0)
ReasoningChain    // Chain of reasoning
Contradiction     // Logical contradiction

Collection Types

List<T>            // Ordered collection
StructuredReport   // Structured output

Type Compatibility Matrix

Can Substitute

FactualClaim    →  String         ✅
CitedFact       →  FactualClaim   ✅
RiskScore       →  Float          ✅
ConfidenceScore →  Float          ✅
StructuredReport → Any output     ✅

Cannot Substitute

Opinion         →  FactualClaim   ❌ (Compile error)
Speculation     →  FactualClaim   ❌ (Compile error)
Float           →  RiskScore      ❌ (Compile error)

Uncertainty Taints

Uncertainty + T  →  Uncertainty   ⚠️  (Propagates)

Complete Examples

Domain Model

type RiskScore(0.0..1.0)

type Party {
  name: FactualClaim,
  role: FactualClaim
}

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

type Contract {
  parties: List<Party>,
  risks: List<Risk>,
  summary: Summary
}

flow AnalyzeContract(doc: Document) -> Contract {
  step Extract {
    probe doc for [parties, risks]
    output: EntityMap
  }
}

Epistemic Constraints

// Only accept factual claims
type FactualReport {
  findings: List<FactualClaim>,   // Must be facts
  analysis: RiskScore,            // Quantified risk
  sources: List<CitedFact>        // Must cite sources
}

// Opinions are separated
type Commentary {
  expert_opinion: Opinion,         // Clearly marked as opinion
  confidence: ConfidenceScore
}

Range and Refinement

type ValidScore(0.0..100.0) where value >= 50.0

type HighConfidenceResult {
  value: FactualClaim,
  confidence: ConfidenceScore
} where confidence >= 0.85

flow ValidateScore(input: Float) -> ValidScore {
  step Check {
    given: input
    ask: "Ensure score is valid"
    output: ValidScore
  }
}

Best Practices

1. Use Nominal Types for Domain Concepts

// Good: semantic distinction
type Employee
type Contractor

// Even if they have the same structure
type Employee { name: String, id: String }
type Contractor { name: String, id: String }
// Employee ≠ Contractor (semantic difference)

2. Use Epistemic Types for Information Quality

type Analysis {
  facts: List<FactualClaim>,      // Must be verifiable
  opinions: List<Opinion>,         // Clearly separated
  confidence: ConfidenceScore
}

3. Use Refinement for Constraints

type Score(0.0..1.0) where confidence >= 0.8

type ValidInput where length > 0 ∧ length <= 10000

4. Mark Optional Fields Explicitly

type Party {
  name: FactualClaim,         // Required
  role: FactualClaim,         // Required
  contact: String?,           // Optional
  notes: Opinion?             // Optional
}

5. Prevent Opinion/Fact Confusion

// ❌ Don't mix
type BadReport {
  content: String  // Could be fact or opinion—unclear
}

// ✅ Separate clearly
type GoodReport {
  facts: List<FactualClaim>,
  opinions: List<Opinion>
}

Type Checking

The AXON type checker validates: ✅ Name resolution: All referenced types exist
✅ Epistemic compatibility: Opinion cannot substitute for FactualClaim
✅ Range validity: min < max in range constraints
✅ Field types: All field types are valid
✅ Generic parameters: Generic type arguments are valid

type Invalid(1.0..0.0)  // ❌ Error: min > max

type Bad {
  field: NonExistentType  // ❌ Error: undefined type
}

flow Wrong(input: Opinion) -> FactualClaim {  // ❌ Error: incompatible types
  // Opinion cannot become FactualClaim
}

Types vs. Contracts

Aspect	Types	Contracts
When	Compile-time	Runtime
Purpose	Define validity	Enforce validity
Decidability	Always decidable	Empirically verified
Dependencies	No LLM dependency	May depend on LLM

Example

// Type: defines valid domain
type ValidParty where name ≠ ∅ ∧ role ∈ ValidRoles

// Anchor: enforces LLM produces valid output
anchor PartyExtraction {
  require: source_citation
  confidence_floor: 0.85
}

flow Extract(doc: Document) -> ValidParty {
  step ExtractParty {
    given: doc
    output: ValidParty  // Type constraint
  }
}

run Extract(myDoc)
  constrained_by [PartyExtraction]  // Runtime enforcement

Anchor — Runtime constraints
Flow — Typed cognitive pipelines
Persona — Agent identities
Syntax Overview — Language syntax

​Overview

​Key Principle

​Type Layers

​Layer 1: Nominal Types

​Syntax

​Examples

​When to Use

​Layer 2: Structural Epistemic Types

​Built-in Epistemic Types

​Compatibility Rules

​Example

​Uncertainty Propagation

​Layer 3: Refinement Types

​Range Constraints

​Where Clauses

​Allowed Predicates

​Example

​Layer 4: Dependent Types (Light)

​Planned Syntax

​What’s Allowed

​Type Definition Syntax

​Simple Type

​Structured Type

​Range-Constrained Type

​Refined Type

​Type with Where Clause

​Combining Features

​Type Expressions

​Basic Type Reference

​Generic Types

​Optional Types

​Nested Types

​Generic Type Parameters

​Optional Fields

​Built-in Types

​Primitive Types

​Epistemic Types

​Content Types

​Analysis Types

​Collection Types

​Type Compatibility Matrix

​Can Substitute

​Cannot Substitute

​Uncertainty Taints

​Complete Examples

​Domain Model

​Epistemic Constraints

​Range and Refinement

​Best Practices

​1. Use Nominal Types for Domain Concepts

​2. Use Epistemic Types for Information Quality

​3. Use Refinement for Constraints

​4. Mark Optional Fields Explicitly

​5. Prevent Opinion/Fact Confusion

​Type Checking

​Types vs. Contracts

​Example

​Related

Overview

Key Principle

Type Layers

Layer 1: Nominal Types

Syntax

Examples

When to Use

Layer 2: Structural Epistemic Types

Built-in Epistemic Types

Compatibility Rules

Example

Uncertainty Propagation

Layer 3: Refinement Types

Range Constraints

Where Clauses

Allowed Predicates

Example

Layer 4: Dependent Types (Light)

Planned Syntax

What’s Allowed

Type Definition Syntax

Simple Type

Structured Type

Range-Constrained Type

Refined Type

Type with Where Clause

Combining Features

Type Expressions

Basic Type Reference

Generic Types

Optional Types

Nested Types

Generic Type Parameters

Optional Fields

Built-in Types

Primitive Types

Epistemic Types

Content Types

Analysis Types

Collection Types

Type Compatibility Matrix

Can Substitute

Cannot Substitute

Uncertainty Taints

Complete Examples

Domain Model

Epistemic Constraints

Range and Refinement

Best Practices

1. Use Nominal Types for Domain Concepts

2. Use Epistemic Types for Information Quality

3. Use Refinement for Constraints

4. Mark Optional Fields Explicitly

5. Prevent Opinion/Fact Confusion

Type Checking

Types vs. Contracts

Example

Related