Skip to content

Commit af43c72

Browse files
committed
feat(registry): register Haec (trope-particularity language)
Add languages/haec.md (thin pointer) + index row; portfolio row; a README Projects subsection; a TOOLING-STATUS row; and a clean LANGUAGES.a2ml stanza. Haec is the front-end of the three-repo trope-particularity system (siblings: trope-checker = Idris2 verified core + executable checker; trope-particularity- workbench = the nine-effect vocabulary); shares the loss-with-residue substrate with echo-types. Cut from fresh origin/main.
1 parent 869e1e6 commit af43c72

6 files changed

Lines changed: 61 additions & 0 deletions

File tree

.machine_readable/LANGUAGES.a2ml

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -396,3 +396,13 @@ kind = "Orchestration DSL"
396396
status = "external"
397397
canonical-repo = "hyperpolymath/kitchenspeak"
398398
note = "extracted from this coordinator; in-tree snapshot removed"
399+
400+
# ─── Haec (trope-particularity) — clean stanza added 2026-06-22 ───
401+
[[language]]
402+
id = "haec"
403+
name = "Haec"
404+
repo = "https://github.com/hyperpolymath/haec"
405+
invariant = "Every quality-loss is graded and checked against its use"
406+
role = "Trope-particularity: graded property-instance loss, lowered to a language-neutral Trope IR, use-checked"
407+
ecosystem = ["https://github.com/hyperpolymath/trope-checker", "https://github.com/hyperpolymath/trope-particularity-workbench"]
408+
status = "design"

README.adoc

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -100,6 +100,21 @@ Status: partially implemented.
100100

101101
---
102102

103+
=== Haec
104+
105+
A Turing-complete language whose type discipline is *trope-particularity*: every
106+
operation on a property-instance carries a graded *loss-shape*, lowered to a
107+
language-neutral *Trope IR* and checked against a declared use-model by a separate,
108+
portable checker (`hyperpolymath/trope-checker`, an Idris2 verified core plus an
109+
executable). The named effects, residual, and verdict live in
110+
`hyperpolymath/trope-particularity-workbench`. Shares the loss-with-residue
111+
substrate with `echo-types`.
112+
113+
Status: design (grammar + elaboration + round-tripping examples); the checker's
114+
verified core typechecks with no axioms.
115+
116+
---
117+
103118
=== KitchenSpeak (experimental DSL — moved out)
104119

105120
An experimental, formally-verified orchestration *DSL* for the domestic kitchen,

TOOLING-STATUS.adoc

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -53,6 +53,9 @@ Cross-axis invariants: ARG ≤ TRG always; ARG-A requires FRG ≥ B.
5353
| **JtV** | TBD | TBD | TBD | TBD | TBD | Profile not yet authored.
5454
| **Oblibeny** | TBD | TBD | TBD | TBD | TBD | Profile not yet authored.
5555
| **Error-lang** | TBD | TBD | TBD | TBD | TBD | Profile not yet authored.
56+
| **Haec**
57+
| TBD | TBD | TBD | TBD | FULL
58+
| 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).
5659
| **Kitchenspeak** | TBD | TBD | TBD | TBD | TBD | Proofs commenced (Dough, PoachedEgg, EchoBridge); ADR 0001–0004; echo-types dependency. Profile not yet authored.
5760
| **Tangle** | TBD | TBD | TBD | TBD | TBD | Profile not yet authored.
5861
| **Me-dialect** | TBD | TBD | TBD | TBD | TBD | Profile not yet authored.

docs/language-portfolio.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,7 @@ live in each language's own repo and in the coordinator's canonical trackers:
2828
| My-Lang | `hyperpolymath/my-lang` | Solo → Duet → Ensemble dialect family |
2929
| JtV | `hyperpolymath/jtv` | Systems language, Harvard architecture |
3030
| Error-Lang | `hyperpolymath/error-lang` | Pedagogical, systems thinking via errors |
31+
| Haec | `hyperpolymath/haec` | Trope-particularity: graded property-instance loss, use-checked |
3132
| Oblíbený | `hyperpolymath/oblibeny` | Turing-incomplete secure deployment |
3233
| Anvomidav | `hyperpolymath/anvomidav` | Hard real-time / formal verification |
3334
| betlang | `hyperpolymath/betlang` | Foundational / probabilistic experiment |

languages/README.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ Each language has one core invariant that defines its design philosophy.
1818
| [jtv](jtv.md) | Data and code are strictly separated |
1919
| [affinescript](affinescript.md) | Every resource is used at most once |
2020
| [ephapax](ephapax.md) | Every value can be consumed exactly once |
21+
| [haec](haec.md) | Every quality-loss is graded and checked against its use |
2122

2223
Each row links to a thin pointer; the language itself lives in its own
2324
`hyperpolymath/<lang>` repo. For cross-language status see

languages/haec.md

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
<!--
2+
SPDX-License-Identifier: MPL-2.0
3+
Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
4+
-->
5+
# Haec
6+
7+
> Every quality-loss is graded and checked against its use.
8+
9+
**Canonical repository:** [hyperpolymath/haec](https://github.com/hyperpolymath/haec)
10+
11+
Haec is a Turing-complete language whose type discipline is *trope-particularity*:
12+
every operation on a *property-instance* (a quality as borne by _this_ entity, in
13+
_this_ context) carries a *loss-shape grade*, and the surviving residue is judged
14+
against a declared *use-model*. Haec is one **front-end** of a three-repo system —
15+
it lowers programs to a language-neutral **Trope IR**; it defines neither the
16+
checker nor the vocabulary:
17+
18+
- [hyperpolymath/trope-checker](https://github.com/hyperpolymath/trope-checker)
19+
the portable checker (Idris2 verified core + executable) that consumes the Trope
20+
IR and returns a verdict (`p-sufficient` / `p-insufficient`) with a witness edge.
21+
- [hyperpolymath/trope-particularity-workbench](https://github.com/hyperpolymath/trope-particularity-workbench)
22+
the informal vocabulary (the nine named effects, the residual, the verdict).
23+
24+
Shares the *irreversible-transformation-with-retained-residue* substrate with
25+
[`echo-types`](https://github.com/hyperpolymath/echo-types) (the graded-loss reading
26+
the calculus builds on).
27+
28+
This coordinator only *indexes* the language. The implementation, specification,
29+
grammar, examples, and live status live in the canonical repositories above — not
30+
here. See also [`../.machine_readable/LANGUAGES.a2ml`](../.machine_readable/LANGUAGES.a2ml)
31+
and [`../TOOLING-STATUS.adoc`](../TOOLING-STATUS.adoc).

0 commit comments

Comments
 (0)