|
| 1 | +<!-- |
| 2 | +SPDX-License-Identifier: CC-BY-SA-4.0 |
| 3 | +SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 4 | +--> |
| 5 | + |
| 6 | +[](https://opensource.org/licenses/MPL-2.0)  |
| 8 | + |
| 9 | +<div class="lead" wrapper="1"> |
| 10 | + |
| 11 | +A Turing-complete language whose type discipline is |
| 12 | +**trope-particularity**. |
| 13 | + |
| 14 | +</div> |
| 15 | + |
| 16 | +> [!NOTE] |
| 17 | +> Working name. The project is the **language**, not the checker and not |
| 18 | +> the vocabulary; **Haec** (from *haecceity*, "thisness") is a |
| 19 | +> placeholder — rename freely. |
| 20 | +
|
| 21 | +> Duck typing asks whether it quacks. A trope language lets you write |
| 22 | +> the program that decides which quack to keep — and the checker tells |
| 23 | +> you, against each consumer’s declared use, whether the quack you kept |
| 24 | +> was enough. |
| 25 | +
|
| 26 | +<div id="toc"> |
| 27 | + |
| 28 | +</div> |
| 29 | + |
| 30 | +# What Haec is |
| 31 | + |
| 32 | +Haec is a general-purpose, Turing-complete language (it has general |
| 33 | +recursion) in which every operation over a **property-instance** — a |
| 34 | +quality as borne by this entity, in this context, under these conditions |
| 35 | +— carries a **loss-shape grade**. The grade records what the operation |
| 36 | +did to the instance’s individuating content: how much was retained, |
| 37 | +whether the quality–bearer bond held, whether plurality was merged, and |
| 38 | +whether what is presented is true. |
| 39 | + |
| 40 | +Haec does not decide whether a flow is acceptable. It **produces** a |
| 41 | +record of graded effects — the **Trope IR** — and the |
| 42 | +(language-independent) **tropechecker** consumes that IR and returns a |
| 43 | +verdict against each consumer’s declared use-model. Turing-completeness |
| 44 | +lives in Haec’s terms; decidability lives in the checker’s grade |
| 45 | +algebra. The two never meet: the checker never executes a Haec program, |
| 46 | +so Rice’s theorem is no obstacle — an unbounded lossy loop simply gets |
| 47 | +an honest "unknown" (`top`) grade, which any demanding use rejects. |
| 48 | + |
| 49 | +# What Haec is not |
| 50 | + |
| 51 | +- **Not the tropechecker.** The checker is a separate, portable artefact |
| 52 | + (`github.com/hyperpolymath/trope-checker`). Haec is **one** producer |
| 53 | + of its input among potentially many — a static analyser for another |
| 54 | + language could emit the same IR. Keeping the checker out of this |
| 55 | + repository is deliberate: its guarantee must be a guarantee about the |
| 56 | + IR, not "the Haec checker." |
| 57 | + |
| 58 | +- **Not the vocabulary.** The named effects, the residual, and the |
| 59 | + verdict are defined in the Particularity workbench |
| 60 | + (`github.com/hyperpolymath/trope-particularity-workbench`). Haec |
| 61 | + **implements** those terms; it does not define them. |
| 62 | + |
| 63 | +- **Not "trope safety" as a rival to type safety.** Haec adds a |
| 64 | + diagnostic layer **over** ordinary typing, not a replacement for it. |
| 65 | + |
| 66 | +# Where it sits — the three-repo picture |
| 67 | + |
| 68 | +<div wrapper="1" options="hardbreaks"> |
| 69 | + |
| 70 | +**Haec (this repo)** — writes & type-checks programs; **emits** Trope |
| 71 | +IR.\ |
| 72 | +│ emits\ |
| 73 | +▼**Trope IR** — a graded-effect DAG (the wire format / trust boundary).\ |
| 74 | +│ consumed by\ |
| 75 | +▼**trope-checker** — composes grades, checks each consumer’s use-model, |
| 76 | +returns a\ |
| 77 | +verdict (`p-sufficient` / `p-insufficient`) with a witness edge. |
| 78 | + |
| 79 | +</div> |
| 80 | + |
| 81 | +Both Haec and the checker **realise** the **Particularity** vocabulary; |
| 82 | +the **formal calculus** (grade algebra, IR semantics, soundness) is |
| 83 | +normative in `trope-checker/spec/calculus.adoc`, which this repository |
| 84 | +references rather than restates. See |
| 85 | +`docs/trope-estate-architecture.svg`. |
| 86 | + |
| 87 | +# The type discipline (summary; the normative spec lives with the checker) |
| 88 | + |
| 89 | +The judgement is `Γ` `⊢` `e` `:` `A` `!` `g` — *e* produces an *A* with |
| 90 | +loss-shape grade *g*. The grade is a dependent record over a |
| 91 | +**recoverability × veridicality** space; the bond coordinate fibres over |
| 92 | +whether the bearer survives, so incoherent states (bearer present yet |
| 93 | +bond severed) are not representable. The honest fragment is generated by |
| 94 | +**five atomic moves** — `attenuate`, `predicate`, `drop`, `sever`, |
| 95 | +`fuse` — and the familiar surface effects (`preserve`, `project`, |
| 96 | +`collapse`, `detach`) are sugar over them; the deceptive fragment has |
| 97 | +exactly three values, and none is writable in source (an untagged merge, |
| 98 | +a value-substitution, or a mis-attribution is a **lowering fault**, not |
| 99 | +a program). General recursion takes the least-fixed-point grade, with an |
| 100 | +**unknown** (`top`) grade as the honest answer for unbounded loss. |
| 101 | +Checking is **bidirectional**: declared loss-signatures at recursive and |
| 102 | +effectful boundaries, inference through the straight-line fragment. |
| 103 | + |
| 104 | +Haec’s own job is the part the calculus leaves to a front-end: a surface |
| 105 | +syntax (`design/grammar.ebnf`), and an **elaboration** |
| 106 | +(`design/elaboration.adoc`) that lowers each construct to a Trope IR |
| 107 | +effect edge. |
| 108 | + |
| 109 | +> [!IMPORTANT] |
| 110 | +> The checker’s soundness is **relative to faithful lowering**. It |
| 111 | +> cannot verify that a Haec construct claimed to be (say) a `collapse` |
| 112 | +> really is one, nor that a value Haec marks faithful is not in fact |
| 113 | +> falsified — that needs ground truth the checker does not have. |
| 114 | +> **Proving each construct’s lowering faithful is Haec’s obligation**, |
| 115 | +> discharged per construct (`design/elaboration.adoc`) — not something |
| 116 | +> the checker provides. |
| 117 | +
|
| 118 | +# Status |
| 119 | + |
| 120 | +Design. The surface syntax and the elaboration table are the first |
| 121 | +artefacts; `examples/` pairs small programs with the IR they lower to, |
| 122 | +and each lowered IR round-trips through the trope-checker (schema-valid, |
| 123 | +expected verdict). There is no compiler yet — `compiler/` and `lsp/` are |
| 124 | +named future work (`STATUS.adoc`). |
| 125 | + |
| 126 | +# Repository map |
| 127 | + |
| 128 | +| Path | What lives there | |
| 129 | +|----|----| |
| 130 | +| `README.adoc` | This file. | |
| 131 | +| `design/grammar.ebnf` | The surface grammar. | |
| 132 | +| `design/elaboration.adoc` | The elaboration-to-IR table (+ per-construct O2 obligations). | |
| 133 | +| `design/trope-ir.schema.json` | Vendored copy of the IR contract Haec targets (canonical in trope-checker). | |
| 134 | +| `examples/` | Small programs (`*.haec`) paired with the IR they lower to (`*.ir.json`). | |
| 135 | +| `docs/trope-estate-architecture.svg` | The three-repo dependency picture. | |
| 136 | +| `compiler/` | (planned) Parser, type-checker, elaborator, codegen — see `STATUS.adoc`. | |
| 137 | +| `lsp/` | (planned) Editor support — see `STATUS.adoc`. | |
| 138 | + |
| 139 | +# Run the checks |
| 140 | + |
| 141 | +```sh |
| 142 | +just check # validate examples/*.ir.json against the vendored IR schema |
| 143 | +# full round-trip (verdicts) needs a checkout of the sibling trope-checker: |
| 144 | +../trope-checker/src/idris2/build/exec/tropecheck examples/survey-collapse.ir.json |
| 145 | +``` |
| 146 | + |
| 147 | +# Licence |
| 148 | + |
| 149 | +Code, config, and the vendored schema: Mozilla Public License 2.0. Prose |
| 150 | +documentation: CC-BY-SA-4.0. Per-file `SPDX-License-Identifier` headers |
| 151 | +are authoritative; the single GitHub badge is MPL-2.0 from the root |
| 152 | +`LICENSE`. |
0 commit comments