Haec

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.

Table of Contents

• What Haec is
• What Haec is not
• Where it sits — the three-repo picture
• The type discipline (summary; the normative spec lives with the checker)
• Status
• Repository map
• Run the checks
• Licence

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

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

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

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.