dev.constructive.eo.iron

Prisms for Iron refinements.

A refinement checked at runtime is a partial conversion A ⇀ A :| C with a total way back, and that is exactly a Prism: getOption tests the constraint (hit = the refined value, miss = the untouched source), reverseGet forgets it. Both Prism laws hold for any pure constraint — a value that passed the test passes it again, and forgetting a refinement gives back the very value that was refined.

Each constructor needs only Iron's RuntimeConstraint, which Iron derives from any compile-time Constraint at a call site where the types are concrete, so every built-in and user-defined constraint qualifies. Refinements Iron proves at compile time (refine on a literal) need no optic: they cannot miss.

 import io.github.iltotore.iron.constraint.numeric.Positive

 val positive = IronPrism[Int, Positive]
 positive.getOption(42)                        // Some(42: Int :| Positive)
 positive.getOption(-1)                        // None

 // Lens ∘ Prism = Optional: only valid ages get written.
 val age = Lens[Person, Int](_.age, (p, a) => p.copy(age = a)).andThen(positive)

 // Traversal ∘ Prism = filtering Traversal: only the positive elements are visited.
 Traversal.each[List, Int].andThen(positive).foldMap(List(_))(List(3, -1, 4))  // List(3, 4)

The constructors return the stock optics.MendTearPrism, so every fused composition and capability mixin of the core Prism applies unchanged. Like every Prism, a miss is a silent pass-through on write; when the reason matters, Iron's own refineEither carries the constraint's message. The .prism extension (import dev.constructive.eo.iron.prism) builds the same Prism from a RuntimeConstraint or Constraint instance.