Repository navigation
docs(research): distinguish gate levels and explore identity across representations and time - #135
Conversation
|
Warning Review limit reachedYou've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Next included review available in 33 minutes. View limit details
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 8cbd0a4fab
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| `routes/alpha-extend/README.adoc` and | ||
| `routes/delta-aggregate/TYPELL-BRIDGE.adoc`. | ||
| Kategoria's first ten *type-theoretic capabilities* are basic types, | ||
| ADTs, polymorphism, type classes, GADTs, dependent types, linear types, |
There was a problem hiding this comment.
The referenced Kategoria taxonomy defines level 4 as Higher-Kinded Types, not type classes. Since this section is intended to distinguish the exact meanings of two numbered schemes, substituting a related but different capability makes the crosswalk factually inaccurate; replace “type classes” with “higher-kinded types.”
Useful? React with 👍 / 👎.
| This L0–L10 is the existing, fixed *VCL-UT query safety / wire | ||
| compatibility* numbering. It is NOT the Kategoria 1–10 language-feature |
There was a problem hiding this comment.
This labels the entire L0–L10 range as query-safety numbering even though docs/2026-07-21-workup-consonance-and-verisim.adoc explicitly identifies L10 EpistemicSafe as not being a query-safety property, but rather a property about whether an answer is warranted. Because L10 is included in the range being defined here, this wording reintroduces the category confusion the new section is meant to eliminate; describe it as statement/gate safety or explicitly carve out L10.
Useful? React with 👍 / 👎.
…s without claiming equivalence
…scribing a single architecture
hyperpolymath
changed the title
|
Scope correction
This PR distinguishes VCL-UT's compatibility-sensitive L0–L10 query-safety predicates from Kategoria's different type-feature taxonomy and TypeLL's other property levels. It does not cap VCL-UT's future research at ten type systems.
It also adds an exploratory, non-normative note,
docs/research/TYPE-TROPE-IDENTITY-SPACES.adoc, in response to the research motivation behind this language: understanding identity and equivalence across representation, context, use and time, not prescribing a universal type/trope framework.Evidence and scope of the new note
Compatibility
Documentation only. No source-language, Idris2/Rust checker, L0–L10 tags, VCLW/VCLS/VCLT wire semantics or runtime policies change.
This note is intended to open the research question without locking a solution in prematurely.