Skip to content

ROADMAP.adoc

Latest commit

 

History

History
218 lines (162 loc) · 8.45 KB

ROADMAP.adoc

File metadata and controls

218 lines (162 loc) · 8.45 KB

TypeLL Roadmap

Table of Contents

Overview

TypeLL is the unified type system verification kernel for the hyperpolymath ecosystem. It is to PanLL what LLVM is to Clang: the formal verification substrate that multiple language frontends compile types into. TypeLL is an open-ended progressive type safety framework: it works through increasingly strong type properties with no fixed upper bound. New levels are added as the theory demands. The initial progression (L1-L10) is defined below and used by VCL-total, 007, Kategoria, PanLL, and the nextgen-languages suite; this is a starting point, not a ceiling.

Current State (2026-03-29)

Architecture

Language Frontends (14 bridges)
        |
        v
typell-core (unified kernel)
  types.rs      — Unified type representation
  unify.rs      — Robinson unification + occurs check
  infer.rs      — Bidirectional type inference
  check.rs      — Type checking coordinator
  linear.rs     — Linear/affine usage tracking (QTT)
  effects.rs    — Algebraic effect system
  qtt.rs        — QTT semiring operations
  dimensional.rs — Dimensional analysis (SI units)
  session.rs    — Session type protocols
  proof.rs      — Proof obligation generation
  error.rs      — Diagnostic types
        |
        v
typell-server (HTTP/JSON-RPC on port 7800)

Rust Workspace (14 crates)

Crate Purpose

typell-core

Unified type kernel (11 modules: types, unify, infer, check, linear, effects, qtt, dimensional, session, proof, error)

typell-server

HTTP/JSON-RPC server (port 7800) with handler dispatch

typell-vcl

VCL-total bridge — maps 10-level type safety into TypeLL (4 modules: lib, bridge, levels, rules)

typell-eclexia

Eclexia language bridge (resource types, dimensional analysis)

typell-affinescript

AffineScript language bridge

typell-ephapax

Ephapax language bridge (linear types)

typell-wokelang

Wokelang language bridge

typell-betlang

Betlang language bridge

typell-mylang

My-Lang language bridge

typell-oblibeny

Oblibeny language bridge

typell-tangle

Tangle language bridge

typell-jtv

JTV language bridge

typell-errorlang

Errorlang language bridge

typell-phronesis

Phronesis language bridge

Progressive Type Safety Hierarchy (Initial Mapping)

Note
 This table documents the initial L1-L10 mapping. TypeLL is open-ended: new levels are added as the type theory demands. L1-L10 is a starting point, not a cap.
Level Name TypeLL Concept

L1

Parse-time safety

Well-formed AST

L2

Schema-binding safety

Named type resolution

L3

Type-compatible operations

Unification + operator checking

L4

Null-safety

Option types, totality checking

L5

Injection-proof safety

Refinement predicates

L6

Result-type safety

Return type inference

L7

Cardinality safety

Bounded quantifiers

L8

Effect-tracking safety

Algebraic effects

L9

Temporal safety

Session types, state machines

L10

Linearity safety

QTT bounded usage, linear types

L11+

Open-ended

Future levels added as theory demands

ABI/FFI Layer

  • Idris2 ABI: src/abi/Types.idr, Layout.idr, Foreign.idr — dependent type proofs for interface correctness

  • Zig FFI: ffi/zig/src/main.zig — C-compatible implementation with integration tests

Consumers

  • VCL-total — Type-safe query language (supersedes VCL-DT); levels 7-10 map VCL-DT legacy extensions

  • 007 — Agent meta-language type system (tropical types, Five Facets); Isabelle foundation complete in tropical-resource-typing (2026-04-11): star equation, Floyd-Warshall, least prefixpoint, CNO — all proved, zero sorry.

  • Kategoria — Category theory verification; Route alpha achieved L9 (session types via Brady indexed monad); research/tropical/ research prototype added referencing tropical-resource-typing proofs.

  • PanLL — Cross-panel type intelligence (TypeLLService + TypeLLEngine in src/core/)

  • typed-wasm — TypeLL progressive type safety applied to WASM memory (current application: L1-L10), multi-module convergence infrastructure for AffineScript + Ephapax

  • nextgen-languages — 14 language frontends via bridge crates

Milestones

v0.1.0 — Core Kernel (COMPLETE)

  • ✓ Unified type representation (HM polymorphism + dependent + linear + effects + sessions + dimensions + refinements)

  • ✓ Robinson unification with occurs check

  • ✓ Bidirectional type inference (synthesis + checking modes)

  • ✓ QTT-based linearity tracking (Zero, One, Omega, Bounded(n))

  • ✓ Algebraic effect system

  • ✓ Dimensional analysis (SI-based, from Eclexia)

  • ✓ Session type protocol duality checking

  • ✓ Proof obligation generation for dependent types

  • ✓ Error diagnostics

  • ✓ #![forbid(unsafe_code)] across all crates

v0.2.0 — Language Bridges (COMPLETE)

  • ✓ 14 language bridge crates (eclexia, affinescript, ephapax, wokelang, betlang, mylang, oblibeny, tangle, jtv, errorlang, phronesis, vcl)

  • ✓ Each bridge: lib.rs + bridge.rs + rules.rs (language-specific type lowering)

  • ✓ VCL-total bridge maps all 10 levels including VCL-DT legacy (linear, session, effects, modal, proof-carrying, QTT)

v0.3.0 — Server & Integration (COMPLETE)

  • ✓ typell-server HTTP/JSON-RPC on port 7800

  • ✓ Handler dispatch for type checking requests

  • ✓ Wire-compatible serialization with PanLL (TypeLLModel.res)

  • ✓ PanLL TypeLLService integration (cross-panel type intelligence)

v0.4.0 — ABI/FFI Layer (COMPLETE)

  • ✓ Idris2 ABI definitions (Types.idr, Layout.idr, Foreign.idr)

  • ✓ Zig FFI implementation (main.zig)

  • ✓ Integration tests (ffi/zig/test/integration_test.zig)

  • ✓ ReScript example (examples/SafeDOMExample.res)

v0.5.0 — Comprehensive Testing (IN PROGRESS)

  • ✓ Core comprehensive tests (crates/typell-core/tests/core_comprehensive_tests.rs)

  • ✓ Integration tests (tests/integration_test.rs)

  • ❏ Cross-bridge type checking tests (verify same type in 2+ languages unifies)

  • ❏ Performance benchmarks (large type graphs, deep unification)

  • ❏ Fuzz testing for unification and inference

v0.6.0 — VCL-total Deep Integration (PLANNED)

  • ❏ VCL-total query type annotations (level metadata in query results)

  • ❏ Type-safe query composition (compose queries with verified type compatibility)

  • ❏ Query result type inference (infer return types from schema + query)

  • ❏ Level escalation tracking (which operations require higher levels)

v0.7.0 — 007 Integration (PLANNED)

  • ❏ 007 agent type checking (tropical types, Five Facets) — math foundation proven in Isabelle (tropical-resource-typing); Idris2 prototype in katagoria/research/tropical/TropicalKleene.idr

  • ❏ Session type verification for agent choreographies

  • ❏ Effect tracking for agent side effects

  • ❏ Linear resource tracking for agent capabilities

v0.8.0 — Production Hardening (PLANNED)

  • ❏ Sub-millisecond type checking for common cases

  • ❏ Incremental type checking (cache + invalidation)

  • ❏ LSP protocol support (IDE integration)

  • ❏ SARIF output for CI/CD integration

  • ❏ Documentation: architecture guide, language bridge development guide

v1.0.0 — Stable Release (PLANNED)

  • ❏ All 14 language bridges fully tested

  • ❏ VCL-total and 007 integrations production-ready

  • ❏ API stability guarantee (no breaking changes to core types)

  • ❏ Performance validated at scale

  • ❏ arXiv paper on TypeLL progressive type safety (open-ended hierarchy)

  • ❏ L10 cubical/HoTT support (requires cubical prover — currently a wall in pure Idris2)

Post-v1.0

  • typed-wasm — TypeLL progressive type safety applied to WASM memory, multi-module breakthrough; also the AffineScript + Ephapax aggregate library

  • Additional language bridges — Ada, Haskell, Rust, Gleam frontends

  • Distributed type checking — Federated TypeLL instances sharing type context

  • Proof search — Automated theorem proving for type obligations (ECHIDNA integration)

  • Academic publication — Graduated type safety as research contribution

License & Governance

License: MPL-2.0 (Palimpsest License)

Author: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>

Last Updated: 2026-04-11