hyperpolymath · Jun 25, 2026
@@ -0,0 +1,152 @@
+<!--
+SPDX-License-Identifier: CC-BY-SA-4.0
+SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+-->
+
+[![License: MPL-2.0](https://img.shields.io/badge/License-MPL_2.0-blue.svg)](https://opensource.org/licenses/MPL-2.0) ![Status:
+design](https://img.shields.io/badge/status-design-orange)
+
+<div class="lead" wrapper="1">
+
+A Turing-complete language whose type discipline is
+**trope-particularity**.
+
+</div>
+
+> [!NOTE]
+> Working name. The project is the **language**, not the checker and not
+> the vocabulary; **Haec** (from *haecceity*, "thisness") is a
+> placeholder — rename freely.
+
+> Duck typing asks whether it quacks. A trope language lets you write
+> the program that decides which quack to keep — and the checker tells
+> you, against each consumer’s declared use, whether the quack you kept
+> was enough.
+
+<div id="toc">
+
+</div>
+
+# What Haec is
+
+Haec is a general-purpose, Turing-complete language (it has general
+recursion) in which every operation over a **property-instance** — a
+quality as borne by this entity, in this context, under these conditions
+— carries a **loss-shape grade**. The grade records what the operation
+did to the instance’s individuating content: how much was retained,
+whether the quality–bearer bond held, whether plurality was merged, and
+whether what is presented is true.
+
+Haec does not decide whether a flow is acceptable. It **produces** a
+record of graded effects — the **Trope IR** — and the
+(language-independent) **tropechecker** consumes that IR and returns a
+verdict against each consumer’s declared use-model. Turing-completeness
+lives in Haec’s terms; decidability lives in the checker’s grade
+algebra. The two never meet: the checker never executes a Haec program,
+so Rice’s theorem is no obstacle — an unbounded lossy loop simply gets
+an honest "unknown" (`top`) grade, which any demanding use rejects.
+
+# What Haec is not
+
+- **Not the tropechecker.** The checker is a separate, portable artefact
+  (`github.com/hyperpolymath/trope-checker`). Haec is **one** producer
+  of its input among potentially many — a static analyser for another
+  language could emit the same IR. Keeping the checker out of this
+  repository is deliberate: its guarantee must be a guarantee about the
+  IR, not "the Haec checker."
+
+- **Not the vocabulary.** The named effects, the residual, and the
+  verdict are defined in the Particularity workbench
+  (`github.com/hyperpolymath/trope-particularity-workbench`). Haec
+  **implements** those terms; it does not define them.
+
+- **Not "trope safety" as a rival to type safety.** Haec adds a
+  diagnostic layer **over** ordinary typing, not a replacement for it.
+
+# Where it sits — the three-repo picture
+
+<div wrapper="1" options="hardbreaks">
+
+**Haec (this repo)** — writes & type-checks programs; **emits** Trope
+IR.\
+│ emits\
+▼**Trope IR** — a graded-effect DAG (the wire format / trust boundary).\
+│ consumed by\
+▼**trope-checker** — composes grades, checks each consumer’s use-model,
+returns a\
+verdict (`p-sufficient` / `p-insufficient`) with a witness edge.
+
+</div>
+
+Both Haec and the checker **realise** the **Particularity** vocabulary;
+the **formal calculus** (grade algebra, IR semantics, soundness) is
+normative in `trope-checker/spec/calculus.adoc`, which this repository
+references rather than restates. See
+`docs/trope-estate-architecture.svg`.
+
+# The type discipline (summary; the normative spec lives with the checker)
+
+The judgement is `Γ` `⊢` `e` `:` `A` `!` `g` — *e* produces an *A* with
+loss-shape grade *g*. The grade is a dependent record over a
+**recoverability × veridicality** space; the bond coordinate fibres over
+whether the bearer survives, so incoherent states (bearer present yet
+bond severed) are not representable. The honest fragment is generated by
+**five atomic moves** — `attenuate`, `predicate`, `drop`, `sever`,
+`fuse` — and the familiar surface effects (`preserve`, `project`,
+`collapse`, `detach`) are sugar over them; the deceptive fragment has
+exactly three values, and none is writable in source (an untagged merge,
+a value-substitution, or a mis-attribution is a **lowering fault**, not
+a program). General recursion takes the least-fixed-point grade, with an
+**unknown** (`top`) grade as the honest answer for unbounded loss.
+Checking is **bidirectional**: declared loss-signatures at recursive and
+effectful boundaries, inference through the straight-line fragment.
+
+Haec’s own job is the part the calculus leaves to a front-end: a surface
+syntax (`design/grammar.ebnf`), and an **elaboration**
+(`design/elaboration.adoc`) that lowers each construct to a Trope IR
+effect edge.
+
+> [!IMPORTANT]
+> The checker’s soundness is **relative to faithful lowering**. It
+> cannot verify that a Haec construct claimed to be (say) a `collapse`
+> really is one, nor that a value Haec marks faithful is not in fact
+> falsified — that needs ground truth the checker does not have.
+> **Proving each construct’s lowering faithful is Haec’s obligation**,
+> discharged per construct (`design/elaboration.adoc`) — not something
+> the checker provides.
+
+# Status
+
+Design. The surface syntax and the elaboration table are the first
+artefacts; `examples/` pairs small programs with the IR they lower to,
+and each lowered IR round-trips through the trope-checker (schema-valid,
+expected verdict). There is no compiler yet — `compiler/` and `lsp/` are
+named future work (`STATUS.adoc`).
+
+# Repository map
+
+| Path | What lives there |
+|----|----|
+| `README.adoc` | This file. |
+| `design/grammar.ebnf` | The surface grammar. |
+| `design/elaboration.adoc` | The elaboration-to-IR table (+ per-construct O2 obligations). |
+| `design/trope-ir.schema.json` | Vendored copy of the IR contract Haec targets (canonical in trope-checker). |
+| `examples/` | Small programs (`*.haec`) paired with the IR they lower to (`*.ir.json`). |
+| `docs/trope-estate-architecture.svg` | The three-repo dependency picture. |
+| `compiler/` | (planned) Parser, type-checker, elaborator, codegen — see `STATUS.adoc`. |
+| `lsp/` | (planned) Editor support — see `STATUS.adoc`. |
+
+# Run the checks
+
+```sh
+just check     # validate examples/*.ir.json against the vendored IR schema
+# full round-trip (verdicts) needs a checkout of the sibling trope-checker:
+../trope-checker/src/idris2/build/exec/tropecheck examples/survey-collapse.ir.json
+```
+
+# Licence
+
+Code, config, and the vendored schema: Mozilla Public License 2.0. Prose
+documentation: CC-BY-SA-4.0. Per-file `SPDX-License-Identifier` headers
+are authoritative; the single GitHub badge is MPL-2.0 from the root
+`LICENSE`.