dev.constructive.eo.laws

Law equations for an AffineFold[S, A] — a read-only 0-or-1 focus optic whose carrier is Affine and whose write side is pinned to Unit.

AffineFold's observable surface is two operations — getOption and foldMap — and the laws below pin down their agreement:

1. getOptionConsistent: getOption and foldMap agree on the single hit. Phrased via foldMap(List(_)): the full fold collects every focus into a list; for AffineFold that list has zero or one element, whose head is exactly the getOption result.
2. missIsEmpty: when getOption(s) is None, foldMap(f)(s) must equal Monoid.empty under every monoid M. Tested at Int (additive) for scalacheck coverage.
3. hitIsSingleton: when getOption(s) is Some(a), foldMap(f)(s) must equal f(a) under every monoid. Tested at Int as above.

Laws (2) and (3) are the two "branches" of an invariant that's trivially true by the Affine carrier's ForgetfulFold instance — they're nonetheless worth stating because the AffineFold's value is exactly that a user-supplied partial matcher fits the miss/hit contract. A constructor that returned the wrong branch would fail law (2) or (3) for the wronged input.

Ported from Monocle's monocle.law.AffineFoldLaws (which states getAll.headOption === getOption directly); our phrasing goes through the generic foldMap extension to stay within the existential-optic surface.

Law equations for a Fold[S, A] — a read-only optic whose carrier F has ForgetfulFold[F] and whose write-side is pinned to Unit.

These laws encode the two universal properties of any monoidal fold — foldMap(const(mempty)) collapses to mempty, and foldMap is a monoid homomorphism in the target monoid. The homomorphism property is stated here (additive Int monoid, sufficient to witness the law); see also dev.constructive.eo.laws.eo.FoldMapHomomorphismLaws which states it for any optic with ForgetfulFold[F] and is reused by Traversal / Lens. FoldLaws re-states the empty-constant variant here because it is a genuine stand-alone property of Fold that does not need the homomorphism law's two-function phrasing.

Note: FoldLaws does not include a foldMap consistency check against an externally-supplied Foldable[F]. For Fold.apply[F, A] that consistency is a corollary of how the carrier Forget[F] wires its ForgetfulFold instance through Foldable[F].foldMap. Users who want that check should exercise it as a spec-level property test against the concrete constructor.

Law equations for a Getter[S, A] — Optic[S, Unit, A, Unit, Direct].

A Getter is a read-only optic: both its leftover T and its back-focus B are Unit so no write path exists (and so Getters compose through the ordinary andThen). The only observable behaviour is get, which makes the meaningful law a constructor-correctness check: getter.get(s) must equal whatever reference function the caller claims the getter represents. This rules out plumbing mistakes like swapping _._1 / _._2 or accidentally threading the input through identity.

Compared to Monocle's GetterLaws, we omit the fold-consistency law (getter.fold.getAll(s).headOption == Some(getter.get(s))). The Composer[Direct, Forget[F]] bridge it needs exists (dev.constructive.eo.optics.Unfold made Forget[F]'s from a sound singleton-pick), so a Getter→Fold morph is available; the law is simply not yet restated here.

Law equations for an Iso[S, A] — Optic[S, S, A, A, Direct].

Ported from Monocle's monocle.law.IsoLaws. Where Monocle spells iso.get(s) / iso.reverseGet(a) directly, EO's iso is an Optic whose Direct carrier yields the same operations through the Accessor / ReverseAccessor extensions. The content of the laws is identical; only the carrier spelling changes.

modifyIdentity / composeModify for Iso are direct corollaries of the two round-trip laws (modify = from ∘ f ∘ to), so this trait does not enumerate them separately. They are also awkward to express with EO's existential encoding because the Direct type alias has no Bifunctor, so it does not reach the generic ForgetfulFunctor derivation that the modify extension drives off.

Law equations for a Lens[S, A] — Optic[S, S, A, A, Tuple2].

Ported from Monocle's monocle.law.LensLaws. Six equations total: the three classical get/replace round-trips plus modify identity, modify composition, and the consistency bridge between replace and modify.

Law equations for a Modify[S, A] — Optic[S, S, A, A, ModifyF].

Ported from Monocle's monocle.law.SetterLaws. Modify optics have no get, so the four laws are modify-only: identity, composition, replace idempotence, and the consistency of replace with modify(const a).

Laws for MultiFocus[F][S, A] — Optic[S, S, A, A, MultiFocus[F]] — at a concrete F[_].

• MF1 modifyIdentity — mf.modify(identity)(s) == s.
• MF2 composeModify — mf.modify(g) ∘ mf.modify(f) == mf.modify(f andThen g).
• MF3 collectViaMap — mf.collectMap[A](agg)(s) == F.map(s)(_ => agg(s)) at the generic MultiFocus.apply[F, A] factory.
• MF4 collectWithSubsumesCollectMap — mf.collectWith(fa => _ => agg(fa)) == mf.collectMap(agg).
• MF5 collectWithSubsumesModify — mf.collectWith(_ => f) == mf.modify(f).

Law equations for an Optional[S, A] — Optic[S, S, A, A, Affine].

Ported from Monocle's monocle.law.OptionalLaws. getOption is recovered from EO's primitive to, whose Affine carrier is a Miss/Hit sum — fold projects out the focused value when present.

Law equations for a dev.constructive.eo.optics.Plated instance.

These are the unconditional checks — they hold for any S and validate the three moving parts at once: the self-traversal plate (round-trips), transform (identity-preserving), and universe / children (mutually consistent). Running them on a macro-derived plate[S] is the primary correctness signal for the derivation; rewrite needs a terminating rule and so is exercised behaviourally instead of here.

equals is used for the comparisons, so S must have structural equality (every case class / enum does; io.circe.Json does too).

Law equations for a Prism[S, A] — Optic[S, S, A, A, Either].

Ported from Monocle's monocle.law.PrismLaws. The getOption convenience mirrors Monocle's member of the same name, recovered from EO's primitive to: S => Either[S, A].

Laws that exercise an Optional's WRITE SEAM — the generic Optic.modify / Optic.replace (from(map(to(s), _))), the path an UPCAST or COMPOSED write actually takes, NOT any concrete-class convenience surface that might sidestep from.

'''Run these on a DRILLED / partial-cover optic''' — a focus with surrounding context (a field of a larger record, an element beside siblings). A carrier whose from reconstructs the focus STANDALONE (dropping the context) fails seamModifyIdentity here, even though a full-cover fixture passes it trivially. That is precisely the class of bug the full-cover-only Prism / Optional discipline suites could never catch — the 2026-07 avro/circe record-face sibling-drop: Either-carried drilled prisms whose from(Right(b)) = reverseGet(b) threw the siblings away on every composed / upcast write. This law makes that failure loud for any carrier.

Equality is INJECTED because some carriers' S has no lawful universal ==: avro IndexedRecord uses schema-instance-sensitive equals, so pass a structural comparison; circe Json and most value types can pass _ == _.

Law equations for a Traversal[T[_], A] — Optic[T[A], T[A], A, A, MultiFocus[PSVec]].

The MultiFocus[PSVec] carrier carries the right ForgetfulFunctor instance to drive the modify-side laws.

We deliberately do NOT port getAll / headOption here — EO's Optic.all returns the whole container wrapped in a single-element list (cartesian-product semantics from traverse(List(_))), not the individual elements, so Monocle's phrasing of those laws would not be testing what the name suggests.

Law equations for an Unfold[T, B, F] — the build-only / many optic (Optic[Unit, T, Unit, B, Forget[F]] whose real map is embed: F[B] => T).

Like GetterLaws, the primary law is constructor-correctness: the only observable behaviour of a build-only optic is embed, so it must equal whatever reference function the caller claims the unfold represents. The two coherence laws pin the fused andThen members to their specification — post-composition through a Review re-homes the assembled whole ((rev ∘ u).embed = rev.reverseGet ∘ u.embed) and pre-composition maps each part ((u ∘ rev).embed = u.embed ∘ map(rev.reverseGet)) — so an algebra assembled by optic composition cannot drift from the functions it was assembled from.

vestigialSingleton applies only to Applicative-carrier unfolds (built via Unfold.apply): the vestigial read side is pure(()), so a modify round-trip must equal embedding the singleton layer. Pattern-functor unfolds (built via Unfold.algebra) have no lawful read side at all — their vestigial to throws by specification, which is a behaviour check, not a law (see UnfoldSpec).