Skip to content

Commit 4ea7e46

Browse files
hyperpolymathhyperpolymath
authored
Add EXPLAINME document detailing Typell features (#46)
This document provides a detailed claim-to-implementation map, outlining the features and caveats of the Typell system, including type coverage, soundness proofs, and backend implementations. <!-- SPDX-License-Identifier: CC-BY-SA-4.0 --> ## Summary <!-- Briefly describe what this PR does and why. Link to related issues with "Closes #N". --> ## Changes <!-- List the key changes introduced by this PR. --> - ## RSR Quality Checklist <!-- Check all that apply. PRs that fail required checks will not be merged. --> ### Required - [ ] Tests pass (`just test` or equivalent) - [ ] Code is formatted (`just fmt` or equivalent) - [ ] Linter is clean (no new warnings or errors) - [ ] No banned language patterns (no TypeScript, no npm/bun, no Go/Python) - [ ] No `unsafe` blocks without `// SAFETY:` comments - [ ] No banned functions (`believe_me`, `unsafeCoerce`, `Obj.magic`, `Admitted`, `sorry`) - [ ] SPDX license headers present on all new/modified source files - [ ] No secrets, credentials, or `.env` files included ### As Applicable - [ ] `.machine_readable/STATE.a2ml` updated (if project state changed) - [ ] `.machine_readable/ECOSYSTEM.a2ml` updated (if integrations changed) - [ ] `.machine_readable/META.a2ml` updated (if architectural decisions changed) - [ ] Documentation updated for user-facing changes - [ ] `docs/TOPOLOGY.md` updated (if architecture changed) - [ ] `CHANGELOG` or release notes updated - [ ] New dependencies reviewed for license compatibility (MPL-2.0 / MPL-2.0) - [ ] ABI/FFI changes validated (`src/abi/` and `ffi/zig/` consistent) ## Testing <!-- Describe how you tested these changes. --> ## Screenshots <!-- If applicable, add screenshots or terminal output demonstrating the change. --> Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>
1 parent e42d323 commit 4ea7e46

1 file changed

Lines changed: 136 additions & 0 deletions

File tree

‎EXPLAINME-new.adoc‎

Lines changed: 136 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,136 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
= Typell — EXPLAINME
3+
:toc: preamble
4+
:toc-title: Contents
5+
:icons: font
6+
:doctype: article
7+
8+
This file backs every factual claim in link:README.adoc[README.adoc] with code paths and honest caveats. Read it if you are doing due diligence on whether the story matches the code.
9+
10+
== Claim-to-implementation map
11+
12+
=== Typell provides dependent, linear, session, quantitative, effect, and modal type coverage
13+
14+
[quote, README.adoc]
15+
____
16+
Dependent types, linear types, session types, QTT, effect systems, modal types, proof-carrying code.
17+
____
18+
19+
How this is implemented::
20+
The Idris 2 formal specifications in `link:src/abi/[]` define the type system interfaces and soundness properties. The Rust kernel in `link:src/kernel/[]` implements the bidirectional type checker, proof engine, effect tracker, and session protocol manager.
21+
22+
Caveat::
23+
**Phase 0 status.** The Idris 2 specs define the *target* type system. The Rust kernel implementation is under active development. Coverage is by design, not by current achievement.
24+
25+
=== Idris 2 specs prove soundness with zero believe_me
26+
27+
[quote, README.adoc]
28+
____
29+
Dependent types prove type system soundness. Zero believe_me.
30+
____
31+
32+
How this is implemented::
33+
`link:src/abi/[]` contains Idris 2 modules specifying the type system. The `believe_me` count is verified by CI (grep for `believe_me` in `src/abi/`).
34+
35+
Caveat::
36+
The specs prove soundness of the *type system definition*. They do not prove soundness of the Rust implementation. Alignment between spec and implementation is a manual obligation, mitigated by the FFI bridge and generated C headers.
37+
38+
=== The LLVM analogy: any frontend can consume Typell
39+
40+
[quote, README.adoc]
41+
____Typell is to PanLL what LLVM is to Clang: the compiler infrastructure that any frontend can consume.____
42+
43+
How this is implemented::
44+
Typell exposes a JSON-RPC verification protocol (`link:src/kernel/protocol/[]`). PanLL, VS Code extensions, CLI tools, and CI/CD pipelines all consume Typell through this protocol.
45+
46+
Caveat::
47+
The LLVM analogy is architectural, not operational. LLVM has hundreds of production frontends and backends. Typell has one primary consumer (PanLL) under development. The analogy describes the *design intent*, not the current ecosystem.
48+
49+
=== Three language backends target specific database paradigms
50+
51+
[quote, README.adoc]
52+
____VCL-dt++ (VeriSimDB), GQL-dt++ (LithoGlyph), KRL-dt++ (QuandleDB)____
53+
54+
How this is implemented::
55+
Backend directories exist in `link:src/backends/[]`. VCL-dt++ is a port from ReScript. GPNL-dt++ bridges to Lean 4. KRL-dt++ is designed from scratch.
56+
57+
Caveat::
58+
**These backends are in design/early implementation phase.** None are production-ready. The strategies described (8-modality queries, RATIONALE clause, equality saturation) are the target features, not currently shipping capabilities.
59+
60+
=== Zig FFI provides C ABI compatibility
61+
62+
[quote, README.adoc]
63+
____Zig (ffi/zig/): C ABI compatibility per hyperpolymath universal standard.____
64+
65+
How this is implemented::
66+
`link:ffi/zig/[]` contains the Zig FFI layer. Auto-generated C headers live in `link:generated/abi/[]`. The hyperpolymath universal standard is documented in `link:docs/design/ABI-FFI-README.md[]`.
67+
68+
Caveat::
69+
The FFI bridge is the soundness-critical layer. If the Zig FFI misrepresents the Idris 2 spec's types to the Rust kernel, soundness is lost. Integration testing across this boundary is essential and ongoing.
70+
71+
== Dogfooded Across The Account
72+
73+
[cols="1,2,2", options="header"]
74+
|===
75+
| Technology / Pattern | Used here | Also used in
76+
77+
| Idris 2 formal specs
78+
| `src/abi/`
79+
| link:https://github.com/hyperpolymath/kategoria[Kategoria] (Route α)
80+
81+
| Rust kernel
82+
| `src/kernel/`
83+
| link:https://github.com/hyperpolymath/panll[PanLL] (Tauri backend)
84+
85+
| JSON-RPC verification protocol
86+
| `src/kernel/protocol/`
87+
| link:https://github.com/hyperpolymath/panll[PanLL] (Pane-L, Pane-N, Pane-W)
88+
|===
89+
90+
== Known gaps
91+
92+
[CAUTION]
93+
====
94+
**Phase 0: Implementation is beginning.** The architecture, specs, and directory structure exist. The running type checker, proof engine, and backends are under active development.
95+
====
96+
97+
[CAUTION]
98+
====
99+
**Spec-implementation alignment is not machine-checked.** Soundness of the Rust kernel against the Idris 2 specs is a manual obligation. No extraction or certified translation tool exists yet.
100+
====
101+
102+
[CAUTION]
103+
====
104+
**Backend implementations are early.** VCL-dt++, GPNL-dt++, and KRL-dt++ are in design/initial implementation. None handle production query workloads.
105+
====
106+
107+
[CAUTION]
108+
====
109+
**Echidna delegation boundary is underspecified.** Typell delegates complex proofs to Echidna. The boundary between what Typell proves internally and what it delegates is not yet formally delimited.
110+
====
111+
112+
== Evidence Index
113+
114+
[cols="2,3", options="header"]
115+
|===
116+
| Path | Proves / Defines
117+
118+
| `src/abi/`
119+
| Idris 2 formal specs for type system soundness
120+
121+
| `src/kernel/checker/`
122+
| Bidirectional type checker (Rust, under development)
123+
124+
| `src/kernel/proof/`
125+
| Proof engine (Rust, under development)
126+
127+
| `src/kernel/session/`
128+
| Session protocol manager (Rust, under development)
129+
130+
| `docs/design/DESIGN-2026-03-01-typell-vision.md`
131+
| Full design vision document
132+
133+
| `docs/design/ABI-FFI-README.md`
134+
| ABI/FFI standard documentation
135+
|===
136+
abc def ghi jkl mno pqr stu

0 commit comments

Comments
 (0)