diff --git a/.machine_readable/LANGUAGES.a2ml b/.machine_readable/LANGUAGES.a2ml index 24cef43..ad33e2b 100644 --- a/.machine_readable/LANGUAGES.a2ml +++ b/.machine_readable/LANGUAGES.a2ml @@ -396,3 +396,13 @@ kind = "Orchestration DSL" status = "external" canonical-repo = "hyperpolymath/kitchenspeak" note = "extracted from this coordinator; in-tree snapshot removed" + +# ─── Haec (trope-particularity) — clean stanza added 2026-06-22 ─── +[[language]] +id = "haec" +name = "Haec" +repo = "https://github.com/hyperpolymath/haec" +invariant = "Every quality-loss is graded and checked against its use" +role = "Trope-particularity: graded property-instance loss, lowered to a language-neutral Trope IR, use-checked" +ecosystem = ["https://github.com/hyperpolymath/trope-checker", "https://github.com/hyperpolymath/trope-particularity-workbench"] +status = "design" diff --git a/README.adoc b/README.adoc index eec3c63..e975d43 100644 --- a/README.adoc +++ b/README.adoc @@ -100,6 +100,21 @@ Status: partially implemented. --- +=== Haec + +A Turing-complete language whose type discipline is *trope-particularity*: every +operation on a property-instance carries a graded *loss-shape*, lowered to a +language-neutral *Trope IR* and checked against a declared use-model by a separate, +portable checker (`hyperpolymath/trope-checker`, an Idris2 verified core plus an +executable). The named effects, residual, and verdict live in +`hyperpolymath/trope-particularity-workbench`. Shares the loss-with-residue +substrate with `echo-types`. + +Status: design (grammar + elaboration + round-tripping examples); the checker's +verified core typechecks with no axioms. + +--- + === KitchenSpeak (experimental DSL — moved out) An experimental, formally-verified orchestration *DSL* for the domestic kitchen, diff --git a/TOOLING-STATUS.adoc b/TOOLING-STATUS.adoc index 5fd7040..405e75c 100644 --- a/TOOLING-STATUS.adoc +++ b/TOOLING-STATUS.adoc @@ -53,6 +53,9 @@ Cross-axis invariants: ARG ≤ TRG always; ARG-A requires FRG ≥ B. | **JtV** | TBD | TBD | TBD | TBD | TBD | Profile not yet authored. | **Oblibeny** | TBD | TBD | TBD | TBD | TBD | Profile not yet authored. | **Error-lang** | TBD | TBD | TBD | TBD | TBD | Profile not yet authored. +| **Haec** +| TBD | TBD | TBD | TBD | FULL +| Trope-particularity front-end (design pass: grammar + elaboration + round-tripping examples). Siblings: trope-checker (Idris2 verified core + executable checker, conformance), trope-particularity-workbench (the nine-effect vocabulary). | **Kitchenspeak** | TBD | TBD | TBD | TBD | TBD | Proofs commenced (Dough, PoachedEgg, EchoBridge); ADR 0001–0004; echo-types dependency. Profile not yet authored. | **Tangle** | TBD | TBD | TBD | TBD | TBD | Profile not yet authored. | **Me-dialect** | TBD | TBD | TBD | TBD | TBD | Profile not yet authored. diff --git a/docs/language-portfolio.md b/docs/language-portfolio.md index 50e65d9..a13545c 100644 --- a/docs/language-portfolio.md +++ b/docs/language-portfolio.md @@ -28,6 +28,7 @@ live in each language's own repo and in the coordinator's canonical trackers: | My-Lang | `hyperpolymath/my-lang` | Solo → Duet → Ensemble dialect family | | JtV | `hyperpolymath/jtv` | Systems language, Harvard architecture | | Error-Lang | `hyperpolymath/error-lang` | Pedagogical, systems thinking via errors | +| Haec | `hyperpolymath/haec` | Trope-particularity: graded property-instance loss, use-checked | | Oblíbený | `hyperpolymath/oblibeny` | Turing-incomplete secure deployment | | Anvomidav | `hyperpolymath/anvomidav` | Hard real-time / formal verification | | betlang | `hyperpolymath/betlang` | Foundational / probabilistic experiment | diff --git a/languages/README.md b/languages/README.md index 5678cb4..8517e30 100644 --- a/languages/README.md +++ b/languages/README.md @@ -18,6 +18,7 @@ Each language has one core invariant that defines its design philosophy. | [jtv](jtv.md) | Data and code are strictly separated | | [affinescript](affinescript.md) | Every resource is used at most once | | [ephapax](ephapax.md) | Every value can be consumed exactly once | +| [haec](haec.md) | Every quality-loss is graded and checked against its use | Each row links to a thin pointer; the language itself lives in its own `hyperpolymath/` repo. For cross-language status see diff --git a/languages/haec.md b/languages/haec.md new file mode 100644 index 0000000..e666933 --- /dev/null +++ b/languages/haec.md @@ -0,0 +1,31 @@ + +# Haec + +> Every quality-loss is graded and checked against its use. + +**Canonical repository:** [hyperpolymath/haec](https://github.com/hyperpolymath/haec) + +Haec is a Turing-complete language whose type discipline is *trope-particularity*: +every operation on a *property-instance* (a quality as borne by _this_ entity, in +_this_ context) carries a *loss-shape grade*, and the surviving residue is judged +against a declared *use-model*. Haec is one **front-end** of a three-repo system — +it lowers programs to a language-neutral **Trope IR**; it defines neither the +checker nor the vocabulary: + +- [hyperpolymath/trope-checker](https://github.com/hyperpolymath/trope-checker) — + the portable checker (Idris2 verified core + executable) that consumes the Trope + IR and returns a verdict (`p-sufficient` / `p-insufficient`) with a witness edge. +- [hyperpolymath/trope-particularity-workbench](https://github.com/hyperpolymath/trope-particularity-workbench) — + the informal vocabulary (the nine named effects, the residual, the verdict). + +Shares the *irreversible-transformation-with-retained-residue* substrate with +[`echo-types`](https://github.com/hyperpolymath/echo-types) (the graded-loss reading +the calculus builds on). + +This coordinator only *indexes* the language. The implementation, specification, +grammar, examples, and live status live in the canonical repositories above — not +here. See also [`../.machine_readable/LANGUAGES.a2ml`](../.machine_readable/LANGUAGES.a2ml) +and [`../TOOLING-STATUS.adoc`](../TOOLING-STATUS.adoc).