Formal Type System for AI Memory

Schema-Indexed Memory Types and Versioned Evolution

Download: PDF

Overview

This paper establishes the formal type-theoretic foundations for ContextFS's memory system. It defines a rigorous type grammar that enables both runtime (Pydantic) and static (mypy/pyright) type enforcement for AI memory operations.

Type Grammar (Definition 5.1)

The core contribution is a formal grammar for memory types:

BaseType      ::= String | Int | Float | Bool | DateTime | UUID
EntityType    ::= Entity Name Schema
RefType       ::= Ref EntityType
OptionType    ::= Option Type          (T | None)
ListType      ::= List Type            (list[T])
SetType       ::= Set Type             (frozenset[T])
MapType       ::= Map KeyType Value    (dict[K, V])
UnionType     ::= T1 | T2 | ... | Tn
RecordType    ::= {f1: T1, ..., fn: Tn} (Pydantic BaseModel)
MemoryType    ::= Mem Schema           (Generic[S])
VersionedType ::= Versioned MemoryType (with Timeline/ChangeReason)

Mem[S] - Schema-Indexed Memory

The Mem[S] type provides type-safe access to structured memory data:

from contextfs.types import Mem
from contextfs.schemas import DecisionData

# Type-safe property access
typed: Mem[DecisionData] = memory.as_typed(DecisionData)
print(typed.data.decision)   # IDE knows this is str
print(typed.data.rationale)  # Type-safe access

VersionedMem[S] - Evolution Tracking

Memory evolution is tracked through four formal change reasons, each with type-theoretic meaning:

from contextfs.types import VersionedMem, ChangeReason

versioned: VersionedMem[DecisionData] = memory.as_versioned(DecisionData)
versioned.evolve(
    new_content=DecisionData(decision="SQLite", rationale="Simpler"),
    reason=ChangeReason.CORRECTION
)

Timeline Operations

The versioned type supports temporal queries:

# Get version at specific time
past = versioned.timeline.at(datetime(2024, 6, 1))

# Filter by change reason
corrections = versioned.timeline.by_reason(ChangeReason.CORRECTION)

# Get all versions since timestamp
recent = versioned.timeline.since(datetime(2024, 1, 1))

Entity[S] and Ref[E]

For structured entities with lazy-loading references:

from contextfs.types import Entity, Ref

# Create typed entity
user = Entity[UserSchema](
    name="John",
    schema_data=UserSchema(username="johnd", email="john@example.com")
)

# Lazy reference
user_ref: Ref[Entity[UserSchema]] = Ref(user.id, resolver=load_user)
resolved = user_ref.resolve()  # Loads and caches

Theoretical Foundations

The type system draws from:

1. Martin-Löf Type Theory: Dependent types for schema indexing
2. Curry-Howard Correspondence: Types as propositions, terms as proofs
3. Category Theory: Memory operations as morphisms

This enables formal reasoning about memory system correctness and enables IDE tooling to catch type errors at development time.

Implementation

ContextFS implements this type system in Python using:

• Pydantic: Runtime type validation
• Generic types: Static type checking with mypy/pyright
• Protocol classes: Structural subtyping for flexibility

The result is a memory system where type errors are caught both at development time (IDE) and runtime (validation), significantly reducing bugs in AI applications.

References

1. Martin-Löf, P. (1984). Intuitionistic Type Theory
2. Wadler, P. (2015). Propositions as Types. Communications of the ACM
3. Type-Safe Context Engineering - Long, M. (2025)