Skip to content

Commit 9d7b4e8

Browse files
hyperpolymathhyperpolymath
authored
Add Gate 1 adjacency notes for echo types framework
2 parents 3c6f0e9 + f3ba163 commit 9d7b4e8

6 files changed

Lines changed: 489 additions & 0 deletions

File tree

‎docs/adjacency/README.adoc‎

Lines changed: 60 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,60 @@
1+
= Adjacency Notes (Gate 1)
2+
:toc: macro
3+
:sectnums:
4+
5+
[.lead]
6+
One note per neighbouring framework, written to discharge Gate 1 of
7+
`roadmap-gates.adoc`: that echo types name a phenomenon not already
8+
covered elsewhere under a different name.
9+
10+
toc::[]
11+
12+
== Gate 1 test, repeated
13+
14+
For each framework below, the note answers three questions:
15+
16+
. What is the nearest existing construction?
17+
. What do echo types add?
18+
. What do echo types _not_ add?
19+
20+
A framework *fails* the test if every claimed addition is already
21+
present elsewhere under another name. Gate 1 *fails* if no framework
22+
survives the test — in which case the identity claim is retracted per
23+
`roadmap-gates.adoc`.
24+
25+
== Frameworks surveyed
26+
27+
[cols="1,3", options="header"]
28+
|===
29+
| Note | Nearest construction
30+
31+
| link:refinement-types.adoc[Refinement types]
32+
| `{ x : A | P x }` subset types with predicate carrier.
33+
34+
| link:lenses-and-optics.adoc[Lenses and optics]
35+
| get/put pairs with lawful round-tripping.
36+
37+
| link:hott-fibers.adoc[HoTT fibers]
38+
| `fib f y := Σ x , f x = y` with univalent identity.
39+
40+
| link:setoid-quotients.adoc[Setoid quotients]
41+
| `(A , ~)` carrier plus equivalence relation.
42+
43+
| link:provenance-semirings.adoc[Provenance semirings]
44+
| `K`-annotated tuples tracked through relational algebra.
45+
|===
46+
47+
== Reading order
48+
49+
The notes are independent; read whichever framework you already know and
50+
then cross-check the others. If after reading every note you conclude
51+
that echo types are strictly renamed components of one of these
52+
frameworks, Gate 1 fails and the verdict is recorded in
53+
`docs/retractions.adoc`.
54+
55+
== Scope
56+
57+
All notes are written against the current Agda development
58+
(`--safe --without-K`, no postulates). Claims reference specific
59+
theorems by module and name. Anything not backed by a compiled
60+
theorem is called out as conjectural.

‎docs/adjacency/hott-fibers.adoc‎

Lines changed: 89 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,89 @@
1+
= Adjacency: HoTT Fibers
2+
:toc: macro
3+
4+
toc::[]
5+
6+
== 1. Nearest existing construction
7+
8+
In homotopy type theory the fiber of `f : A → B` over `y : B` is
9+
10+
[source]
11+
----
12+
fib f y := Σ (x : A) , (f x = y)
13+
----
14+
15+
This is _definitionally_ the echo construction. On that reading, this
16+
note is where the identity claim is most directly at risk. Everything
17+
below is an argument that the interesting content is not in the
18+
definition but in the intensional setting and the development built
19+
on top of it.
20+
21+
== 2. What do echo types add?
22+
23+
. *Plain intensional setting, no univalence.* The Agda development
24+
uses `--safe --without-K` and `Relation.Binary.PropositionalEquality`.
25+
The `Echo` type family is therefore not claimed to be a ∞-groupoid
26+
or to satisfy function extensionality. Its equalities are the
27+
ordinary intensional ones, and theorems like
28+
`EchoCharacteristic.echo-true≢echo-false` rely on that. A HoTT
29+
reader who treats `fib f y` up to homotopy would _not_ get this
30+
disequality for free; the distinction is intensional.
31+
. *Explicit functorial laws without path induction gymnastics.*
32+
`map-over-id`, `map-over-comp`, `map-square` in
33+
`proofs/agda/Echo.agda` are proved by `refl` and `trans-assoc`, not
34+
by transporting along higher paths. The composition proof
35+
`map-over-comp` is a rewrite on `trans-assoc`; the square proof
36+
`map-square` uses only `cong` and `trans`. These are reusable
37+
outside of a HoTT library.
38+
. *Residue, graded, linear, epistemic extensions sit on top of the
39+
intensional core.* Modules `EchoResidue`, `EchoGraded`,
40+
`EchoLinear`, `EchoEpistemic`, `EchoIntegration` do not require
41+
univalence. They reason about loss in terms of lowerings and
42+
no-section theorems, not in terms of (n-)truncations.
43+
44+
== 3. What do echo types _not_ add?
45+
46+
* *No new mathematical object.* `Echo f y` and `fib f y` are the same
47+
sigma. Anything stated purely about the type former, with no further
48+
structure, is already a HoTT fiber result.
49+
* *No univalent / higher-path content.* The development does not prove
50+
equivalences between fibers in the HoTT sense, does not consider
51+
truncation levels, and does not use higher inductive types.
52+
* *No contractibility-of-fibers style characterisation of
53+
equivalences.* That is a HoTT theorem and remains one.
54+
55+
== 4. Honest risk to the distinction
56+
57+
This is the sharpest adjacency. The honest reading is:
58+
59+
> `Echo = fib`; the identity claim is an _editorial_ claim that
60+
> studying fibers in the intensional, non-univalent setting with an
61+
> emphasis on structured loss is worthwhile in its own right.
62+
63+
Gate 2 (characteristic theorems) and Gate 3 (canonical examples) are
64+
where that editorial claim has to pay its way. If the theorems and
65+
examples turn out to all be corollaries of standard HoTT fiber
66+
results, then this gate fails retrospectively even though the
67+
definitions live in plain Agda.
68+
69+
Two specific stress tests:
70+
71+
. `strict-weakening-collapse` in `EchoResidue`: is there a HoTT
72+
presentation of "certificate with no section back to the fiber"
73+
that subsumes this result? If yes, the residue hierarchy is
74+
renamed HoTT content.
75+
. The epistemic/choreographic/graded bridges: are these specialisations
76+
of HoTT sliced constructions, or are they new compositions?
77+
78+
The current development asserts the former answer is "no" and the
79+
latter is "new composition", but this is the gate most likely to
80+
fail on careful scrutiny.
81+
82+
== 5. Verdict for Gate 1
83+
84+
Marginal pass. The type former is not new. The distinction rests on
85+
the intensional setting, the residue/degradation hierarchy, and the
86+
bridge modules. If Gate 2 or Gate 3 fails, this gate should be
87+
revisited and likely flipped to fail, because the HoTT reader
88+
would be right to treat the whole development as renamed fiber
89+
theory.

‎docs/adjacency/lenses-and-optics.adoc‎

Lines changed: 80 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,80 @@
1+
= Adjacency: Lenses and Optics
2+
:toc: macro
3+
4+
toc::[]
5+
6+
== 1. Nearest existing construction
7+
8+
A lawful lens between `S` and `A` is a pair
9+
10+
[source]
11+
----
12+
get : S → A
13+
put : S → A → S
14+
----
15+
16+
satisfying get-put, put-get, and put-put laws. Prisms, traversals, and
17+
general optics (van Laarhoven, profunctor, indexed, etc.) generalise
18+
this to partial, pluralised, or parameterised access. Optics are the
19+
dominant engineering vocabulary for "structured access to a part of a
20+
larger whole".
21+
22+
The `visible : Bool × Bool → Bool` example in
23+
`proofs/agda/EchoCharacteristic.agda` is in the same neighbourhood as
24+
the "first projection lens" `_1 : Lens (A × B) A`.
25+
26+
== 2. What do echo types add?
27+
28+
. *Explicit source-retention instead of set-back.* A lens carries a
29+
`put` that _reconstructs_ a source from an updated visible value
30+
plus an existing source. Echo types instead _record_ a specific
31+
source alongside the equation `f x ≡ y`. The witness `(true , false)`
32+
in `state₂ : Echo visible true` is a specific retained state, not
33+
the machinery for overwriting one.
34+
. *Asymmetry on the put side.* `no-section-visible` in
35+
`EchoCharacteristic` proves there is no section `Bool → Bool × Bool`
36+
of `visible`. A well-behaved lens's `put` is _not_ a section of
37+
`get`; it is a two-argument update. The echo framing is honest
38+
about the one-argument impossibility and then captures what is
39+
nevertheless retained. Lenses assume a source is already in hand.
40+
. *Composition by commuting square rather than by profunctor.*
41+
`map-square` in `proofs/agda/Echo.agda` transports echoes along a
42+
square `f' ∘ u ≡ v ∘ f`. This is adjacent to lens composition but
43+
the morphism data is different: morphisms of source and target
44+
codomains plus a coherence, not a get/put pair at each step.
45+
. *Residue as first-class lowering.* `EchoResidue.echo-to-residue`
46+
lowers a full echo to a certificate, with
47+
`no-section-collapse-to-residue` witnessing strict loss. Lenses
48+
typically do not ship an analogous quotient-of-the-witness
49+
construction with a non-recoverability proof.
50+
51+
== 3. What do echo types _not_ add?
52+
53+
* No update/`put` operation. Echo types do not say how to overwrite
54+
the visible component or the forgotten component.
55+
* No laws about round-tripping. The lens laws are genuinely more
56+
structured than what the current echo development asks for.
57+
* No profunctor, traversal, or Van Laarhoven encoding. These are
58+
engineering artefacts of optics and have no echo analogue.
59+
* No support for "effectful access" (indexed, monadic, affine optics).
60+
The echo development is pure functions and equalities.
61+
62+
== 4. Honest risk to the distinction
63+
64+
A skeptic can claim that `Echo f y` is the "pre-image half" of a
65+
getter `f`, and that everything interesting here is already implicit
66+
in partial lenses or prisms (which also admit non-existence of a put).
67+
68+
The strongest reply is in the _retention_ semantics: optics are
69+
designed around the ability to reflect an update back, whereas
70+
echoes are designed around the ability to remember what was lost
71+
without reflection. `state₁≢state₂` makes this concrete: two states
72+
with identical visible component and no ability to reconstruct the
73+
second component, yet proof-relevantly distinct on the echo layer.
74+
75+
== 5. Verdict for Gate 1
76+
77+
Survives. Lenses emphasise reversible access; echo types emphasise
78+
witness retention under non-reversibility. The two coincide only at
79+
the get-side skeleton, and diverge immediately on the put/residue
80+
question.

‎docs/adjacency/provenance-semirings.adoc‎

Lines changed: 96 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,96 @@
1+
= Adjacency: Provenance Semirings
2+
:toc: macro
3+
4+
toc::[]
5+
6+
== 1. Nearest existing construction
7+
8+
Green, Karvounarakis, and Tannen introduced K-provenance: database
9+
tuples are annotated by elements of a commutative semiring `K`, and
10+
relational-algebra operations compose annotations using `+` (union),
11+
`·` (join), `0`, `1`. Specialisations include boolean provenance
12+
(which-provenance), `Bag`-provenance (how-many), `Trio`-style
13+
provenance (why/where), and the free semiring `N[X]` (how). The
14+
discipline is "track what each output tuple was derived from, in a
15+
structure that is compositional".
16+
17+
The echo pattern "retain provenance of a visible output under
18+
collapsing computation" is in the same genre.
19+
20+
== 2. What do echo types add?
21+
22+
. *Witness at the level of types, not annotations.* K-provenance
23+
attaches a _label_ to each tuple. Echo types attach a _proof term_
24+
`(x , p)` where `p : f x ≡ y`. The witness is itself an inhabitant
25+
of a dependent type, not a semiring element. This is what
26+
`map-over-id` and `map-over-comp` in `proofs/agda/Echo.agda`
27+
transport.
28+
. *Role-indexed provenance.* `EchoIndexed.Echoᵢ` extends the witness
29+
by a role index so the same visible output can carry different
30+
provenance certificates for different observers. The closest
31+
K-provenance analogue is polynomial provenance with variables per
32+
source, but there the labels are still scalar algebraic terms, not
33+
types indexed by observer.
34+
. *Graded degradation with composition.* `EchoGraded.degrade-comp`
35+
in `proofs/agda/EchoGraded.agda` composes lowerings along
36+
`_≤g_`. K-provenance has a natural homomorphism story ("evaluate in
37+
a simpler semiring"), but a homomorphism between semirings is a
38+
different mathematical object from a typed lowering of witnesses.
39+
. *Strict non-recoverability as a theorem.*
40+
`no-section-collapse-to-residue` in `EchoResidue` _proves_ that the
41+
lowering from echo to residue has no inverse. Provenance
42+
homomorphisms are surjections by construction; the usual framing
43+
does not supply a non-inverse theorem at this granularity.
44+
. *Epistemic integration.* `EchoEpistemic` ties echoes to
45+
observer-indistinguishability and knowledge operators. This is
46+
adjacent to how-provenance but built on different primitives
47+
(`Indist`, `Knows`), not on semiring annotations.
48+
49+
== 3. What do echo types _not_ add?
50+
51+
* No semiring. There is no `+`, no `·`, no `0`, no `1`. The
52+
K-provenance algebra is absent.
53+
* No database-theoretic reading. Relational algebra operators
54+
(projection, selection, join, union) are not instantiated. The
55+
`visible : Bool × Bool → Bool` example is _in the same spirit_ as
56+
projection, but the development does not claim to reconstruct a
57+
provenance-semiring-aware relational algebra.
58+
* No free/polynomial provenance. There is no analogue of `N[X]` that
59+
would let one recover which source contributed how many times.
60+
* No query-equivalence theorems. Provenance theory has powerful
61+
results about when two queries agree on all K-annotations for all
62+
`K`. This is entirely absent here.
63+
64+
== 4. Honest risk to the distinction
65+
66+
A provenance researcher can argue that the residue hierarchy
67+
(`keep`, `residue`, `forget`) is a 3-element bounded lattice and that
68+
`degrade` is a homomorphism into a coarser annotation. On that
69+
reading, everything in `EchoGraded` is "K-provenance for an
70+
impoverished `K`, dressed up as a type family".
71+
72+
There are two non-trivial replies:
73+
74+
. The witnesses are _types_, not semiring elements. `Echo collapse tt`
75+
has two distinct inhabitants that are not identified by any
76+
annotation algebra, because annotations cannot distinguish
77+
`echo-true` from `echo-false` once the semiring is trivial (as it
78+
must be when the output type is `⊤`). The echo framing keeps the
79+
distinction by keeping the source term.
80+
. The bridges (linear, choreographic, epistemic) are not naturally
81+
semiring structures. Attempting to force them into a K-provenance
82+
framing loses the typed content that makes e.g.
83+
`EchoIntegration.knowledge-and-controlled-degradation` go through.
84+
85+
Still, the overlap of _spirit_ is real: both frameworks care about
86+
tracking what survives under lossy operations. The distinction is on
87+
mechanism (types and lowerings vs. semiring annotations), not on
88+
motive.
89+
90+
== 5. Verdict for Gate 1
91+
92+
Survives. The motive overlaps with provenance-semiring work, but the
93+
mechanism is genuinely different. An echo is a proof witness; a
94+
provenance annotation is a semiring element. The two meet in the
95+
middle only via a homomorphism story that no existing work combines
96+
with dependent-type residue hierarchies and epistemic bridges.

0 commit comments

Comments
 (0)