The README makes claims. This file backs them up with evidence.
Typell is the type-theoretic verification engine that powers PanLL’s neurosymbolic intelligence. It provides the "best of the best" type system coverage for formally verified database queries.
Evidence: The README (lines 21-29) lists 7 type system features: 1. Dependent types — types that depend on values (Pi, Sigma) 2. Linear types — resources used exactly once (no data leaks, no double-reads) 3. Session types — protocol safety (connections always closed, transactions atomic) 4. Quantitative Type Theory — resource quantity tracking (rate limits, cost analysis) 5. Effect systems — explicit side effect tracking (read/write/memory) 6. Modal types — contextual access control (transaction-scoped data) 7. Proof-carrying code — cryptographic proof certificates attached to queries
The architecture (lines 46-68) shows Typell as the central verification kernel serving PanLL’s three panes (Pane-L ← constraints, Pane-N ← reasoning, Pane-W ← validated results) plus secondary consumers (VS Code, CLI, CI/CD). This is verifiable in src/kernel/ with modules for type checking, proof engine, effect tracking, session protocol management, and language backends (lines 148-157).
Caveat: Typell is in "Phase 0: Vision capture and repo scaffolding" (line 115). Language backends (VCL-dt, GQL-dt, KQL-dt++) are in design stages; only the kernel architecture exists.
Typell is to PanLL what LLVM is to Clang — the compiler infrastructure that any frontend can consume.
Evidence: The directory structure (lines 136-168) supports this. src/kernel/ is the "middle-end" (type checker, proof engine, effects, session manager). src/backends/ are the language frontends (VCL-dt, GQL-dt, KQL-dt++). integrations/ are the consumers (PanLL primary, VS Code extension, CLI, CI/CD plugins). This mirrors LLVM’s middle-end + backends + frontends architecture.
Caveat: Unlike LLVM (production-ready), Typell’s backends are in design/port stages, not fully functional. Primary investment is in the kernel (bidirectional type checker, proof engine).
| Technology | Learn More |
|---|---|
Rust |
https://www.rust-lang.org (verification kernel, type checker, proof engine) |
Idris2 ABI |
https://www.idris-lang.org (formal specs with dependent type proofs) |
Zig FFI |
https://ziglang.org (C-compatible ABI bridge) |
JSON-RPC |
Protocol for language-agnostic consumer communication |
Tauri 2.0+ |
PanLL desktop backend (Typell verification service) |
Uses the hyperpolymath ABI/FFI standard (Idris2 + Zig). Same pattern across proven, burble, and gossamer.
Typell-specific:
- src/abi/ — Idris2 formal specifications for type system soundness
- ffi/zig/ — C-compatible FFI for cross-language verification calls
- generated/abi/ — Auto-generated C headers from Idris2 ABI
| Path | What’s There |
|---|---|
|
Idris2 formal specifications (type definitions with proofs) |
|
Bidirectional type checker (Pi, Sigma, linear, session types) |
|
Proof engine (generation, verification, caching, certificates) |
|
Effect tracker (read/write/memory side effects) |
|
Session protocol manager (connection safety, transaction atomicity) |
|
JSON-RPC server (consumer communication) |
|
VCL-dt++ backend (VeriSimDB queries with dependent types) |
|
GQL-dt++ backend (LithoGlyph graph queries, Lean 4 bridge) |
|
KQL-dt++ backend (QuandleDB category-theoretic queries) |
|
PanLL primary consumer (pane coordination) |
|
VS Code extension integration |
|
Command-line interface |
|
CI/CD pipeline plugins |
|
Formal specifications (protocol, type-system, proof-system) |
|
Design documents and vision |