diff --git a/README.adoc b/README.adoc deleted file mode 100644 index 25d4233..0000000 --- a/README.adoc +++ /dev/null @@ -1,139 +0,0 @@ -// SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) -// SPDX-License-Identifier: CC-BY-SA-4.0 -// SPDX-License-Identifier: CC-BY-SA-4.0 -= Haec -:revnumber: 0.1 (design) -:revdate: 2026-06-22 -:toc: macro -:toc-placement: preamble - -image:https://img.shields.io/badge/License-MPL_2.0-blue.svg[License: MPL-2.0,link="https://opensource.org/licenses/MPL-2.0"] -image:https://img.shields.io/badge/status-design-orange[Status: design] - -[.lead] -A Turing-complete language whose type discipline is *trope-particularity*. - -NOTE: Working name. The project is the *language*, not the checker and not the -vocabulary; *Haec* (from _haecceity_, "thisness") is a placeholder — rename freely. - -[quote] -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. - -toc::[] - -== 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 - -[%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. - -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] -.Haec's burden: lowering correctness (calculus O2) -==== -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 - -[cols="1,3",options="header"] -|=== -| 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 - -[source,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`. diff --git a/README.md b/README.md new file mode 100644 index 0000000..7a7b6d6 --- /dev/null +++ b/README.md @@ -0,0 +1,152 @@ + + +[![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) + +
+ +A Turing-complete language whose type discipline is +**trope-particularity**. + +
+ +> [!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. + +
+ +
+ +# 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 + +
+ +**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. + +
+ +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`.