# Ornaments Three families of ornament construction over kernel descriptions: raw structural ornaments (`ornament`, `compose`, `forget`, `forgetHoas`, `pullback`, `pullbackHoas`), algebraic ornaments derived from algebras over the supported fragment (`algOrn`, `algShape`, `algSupportedFragment`, `algShapeDiagnostics`, `checkAlgShape`, `liftFold`), and functional ornaments for lifting producers / transforms through canonical output sections (`functional`, `functionalSection`, `functionalTargetIndex`, `functionalBuildIndexed` / `functionalBuild`, `liftProducerIndexed` / `liftProducer`, `liftTransformIndexed` / `liftTransform`, `composeFunctional`). Validation is uniform across families: every constructor has a `validate` / `try` / `diagnose` triple (`validateSpec` / `tryOrnament` / `diagnoseSpec`, `validateAlgOrn` / `tryAlgOrn` / `diagnoseAlgOrn`, `validateFunctional` / `tryFunctional` / `diagnoseFunctional`, plus the law-level `validateFunctionalLaws` / `diagnoseFunctionalLaws`). `validate*` throws on rejection with a structured diagnostic, `try*` returns `{ success; value | diagnostic }`, `diagnose*` always returns the diagnostic record. The supported algebraic fragment is `[ "ret" "arg" "rec" "pi" "plus" ]`. Convenience aliases `section`, `targetIndex`, `buildIndexed`, and `build` re-export the corresponding `functional*` entries for callers writing in the functional-ornament idiom. ## `algOrn` _algOrn: build an algebraic ornament from `args`, running `checkAlgShape` first so unsupported algebra shapes are rejected with structured diagnostics before delegating to `H.algOrn`._ ``` algOrn : { I?, J, baseD | D, erase, algebra, ... } -> Ornament ``` ## `algShape` _algShape: total predicate `{ ok, kind, expected }` over an algebra value's shape — surfaces the offending `kind` when the algebra falls outside `algSupportedFragment`._ ``` algShape : Algebra -> { ok : Bool, kind? : String, expected? : [String] } ``` ## `algShapeDiagnostics` _algShapeDiagnostics: human-readable diagnostic strings for an algebra whose shape falls outside the supported `ret/arg/rec/pi/plus` fragment._ ``` algShapeDiagnostics : Attrs -> [String] ``` ## `algSupportedFragment` _algSupportedFragment: the constructor-tag whitelist `[ "ret" "arg" "rec" "pi" "plus" ]` accepted by `algOrn`; surfaced as the `expected` field of `algShape`'s diagnostic when an algebra falls outside this fragment._ ``` algSupportedFragment : [String] ``` ## `build` _functionalBuild: build the ornamented value from `baseValue` at the unit index `tt` — convenience wrapper for J = `Unit` functional ornaments._ ``` functionalBuild : FunctionalOrnament -> Tm -> Tm ``` ## `buildIndexed` _functionalBuildIndexed: build the ornamented value at an explicit `index` from `baseValue` — wraps `H.ornBuild` for the indexed surface._ ``` functionalBuildIndexed : FunctionalOrnament -> Tm -> Tm -> Tm ``` ## `checkAlgShape` _checkAlgShape: return `algebra` unchanged when it lies in the supported fragment, otherwise throw with the concatenated `algShapeDiagnostics` text._ ``` checkAlgShape : Attrs -> Algebra -- throws on unsupported shape ``` ## `checkSpec` _checkSpec: surface `_ornMeta` from a built ornament — exposes `{ base, spec, core, cfg }` for downstream introspection of the ornament's provenance and shape._ ``` checkSpec : DataSpec -> OrnamentSpec -> Attrs ``` ## `compose` _compose: vertical composition of ornaments at the generic surface — `outer ∘ inner` lifts the inner ornament's J through the outer's K, automatically unpacking `.ornament` cores._ ``` compose : Ornament -> Ornament -> Ornament -- outer, inner ``` ## `composeFunctional` _composeFunctional: vertical composition of two functional ornaments — threads `inner.chooseIndex` and `inner.section` into `outer` to produce a stacked section pipeline._ ``` composeFunctional : FunctionalOrnament -> FunctionalOrnament -> FunctionalOrnament ``` ## `diagnoseAlgOrn` _diagnoseAlgOrn: human-readable diagnostic strings for a candidate algebraic-ornament spec — derived from `H.algOrnDiagnostics`, suitable for error messages and tests._ ``` diagnoseAlgOrn : Attrs -> [String] ``` ## `diagnoseFunctional` _diagnoseFunctional: human-readable diagnostic strings for a candidate functional-ornament spec — derived from `validateFunctional` for surfacing in errors._ ``` diagnoseFunctional : Attrs -> [String] ``` ## `diagnoseFunctionalLaws` _diagnoseFunctionalLaws: human-readable diagnostic strings for failed law checks on a functional ornament — surfaces which law-check returned non-`true` or failed to evaluate._ ``` diagnoseFunctionalLaws : FunctionalOrnament -> [String] ``` ## `diagnoseSpec` _diagnoseSpec: human-readable diagnostic strings for a candidate `(base, spec)` — derived from `H.ornamentDiagnostics`, suitable for error messages and tests._ ``` diagnoseSpec : DataSpec -> OrnamentSpec -> [String] ``` ## `forget` _forget: apply the forgetting morphism to an ornamented `value`, returning the underlying base-description value at the same J-index._ ``` forget : OrnamentedDatatype -> Tm -> Tm ``` ## `forgetHoas` _forgetHoas: yield the HOAS-level `forget` term `J -> ornMu -> baseMu` for an ornamented datatype or raw ornament; prefers `forget0` when the J-index is `Unit`._ ``` forgetHoas : OrnamentedDatatype -> Tm ``` ## `functional` _functional: total smart constructor for a functional ornament — validates `args` via `validateFunctional` and throws with diagnostics on failure, otherwise returns the built record._ ``` functional : Attrs -> FunctionalOrnament -- throws on invalid spec ``` ## `functionalBuild` _functionalBuild: build the ornamented value from `baseValue` at the unit index `tt` — convenience wrapper for J = `Unit` functional ornaments._ ``` functionalBuild : FunctionalOrnament -> Tm -> Tm ``` ## `functionalBuildIndexed` _functionalBuildIndexed: build the ornamented value at an explicit `index` from `baseValue` — wraps `H.ornBuild` for the indexed surface._ ``` functionalBuildIndexed : FunctionalOrnament -> Tm -> Tm -> Tm ``` ## `functionalSection` _functionalSection: extract the `section` slot of a functional ornament — the builder `i -> baseValue -> ornamentedValue` realising the section morphism._ ``` functionalSection : FunctionalOrnament -> (Tm -> Tm -> Tm) ``` ## `functionalTargetIndex` _functionalTargetIndex: extract the `chooseIndex` slot of a functional ornament — the function `i -> baseValue -> J` that picks the ornamented index per base input._ ``` functionalTargetIndex : FunctionalOrnament -> (Tm -> Tm -> Tm) ``` ## `lift` _lift: functorial container lifts — given an ornament `O : Ornament A A'`, `lift.list` / `lift.attrs` / `lift.maybe` produce `Ornament (F A) (F A')` whose forget is the standard functorial action of `F` on `O.forget`; `lift.field name O` is the elementary product-component move. Inputs may be leaf or decorated μ-ornaments; the μ-case delegates element forget to the meta walker._ ``` lift : { list : Ornament -> Ornament, attrs : Ornament -> Ornament, maybe : Ornament -> Ornament, field : String -> Ornament -> Ornament } ``` ## `liftFold` _liftFold: alias for `pullbackHoas` specialised to folds — composes a base fold with `forget` so it runs on ornamented carriers without re-deriving the algebra._ ``` liftFold : OrnamentedDatatype -> (Tm -> Tm) -> Tm -> Tm ``` ## `liftProducer` _liftProducer: lift a base producer through a functional ornament at unit index `tt` — convenience wrapper for J = `Unit`._ ``` liftProducer : FunctionalOrnament -> (Tm -> Tm) -> Tm -> Tm ``` ## `liftProducerIndexed` _liftProducerIndexed: lift a base producer `baseFn : baseInput -> baseValue` through a functional ornament at an explicit J-index, returning the ornamented output._ ``` liftProducerIndexed : FunctionalOrnament -> Tm -> (Tm -> Tm) -> Tm -> Tm ``` ## `liftTransform` _liftTransform: lift a base transform through paired input/output functional ornaments at unit indices — convenience wrapper for J = `Unit` on both sides._ ``` liftTransform : { input, output : FunctionalOrnament, fn } -> Tm -> Tm ``` ## `liftTransformIndexed` _liftTransformIndexed: lift a base transform through paired input/output functional ornaments at explicit indices — auto-unpacks `.ornament` cores from the input side._ ``` liftTransformIndexed : { input, output : FunctionalOrnament, fn } -> Tm -> Tm -> Tm -> Tm ``` ## `ornament` _ornament: user-facing entry — given a generated `DataSpec` (`base`) and a constructor-by-constructor `spec`, produce the ornamented `Datatype` with `forget` morphism baked in._ ``` ornament : DataSpec -> OrnamentSpec -> Datatype ``` ## `pullback` _pullback: apply a base function `baseFn` to a forgotten ornamented value — the value-level companion to `pullbackHoas`, running entirely in HOAS application._ ``` pullback : OrnamentedDatatype -> Tm -> Tm -> Tm ``` ## `pullbackHoas` _pullbackHoas: HOAS-level pullback of a base function `baseFn : I -> baseMu -> R(i)` through an ornamented carrier — auto-unpacks `.ornament` cores from generated datatypes._ ``` pullbackHoas : OrnamentedDatatype -> (Tm -> Tm) -> Tm -> Tm ``` ## `section` _functionalSection: extract the `section` slot of a functional ornament — the builder `i -> baseValue -> ornamentedValue` realising the section morphism._ ``` functionalSection : FunctionalOrnament -> (Tm -> Tm -> Tm) ``` ## `tryAlgOrn` _tryAlgOrn: total constructor — returns `{ ok, diagnostics, value? }` where `value` is the algebraic ornament when valid, otherwise diagnostics-only._ ``` tryAlgOrn : Attrs -> { ok : Bool, diagnostics : [Diagnostic], value? : Ornament } ``` ## `tryFunctional` _tryFunctional: total constructor — returns `{ ok, diagnostics, value? }` where `value` is the built functional ornament when valid, otherwise diagnostics-only._ ``` tryFunctional : Attrs -> { ok : Bool, diagnostics : [Diagnostic], value? : FunctionalOrnament } ``` ## `tryOrnament` _tryOrnament: total constructor — returns `{ ok, diagnostics, value? }` where `value` is the built ornamented datatype when valid, otherwise diagnostics-only._ ``` tryOrnament : DataSpec -> OrnamentSpec -> { ok : Bool, diagnostics : [Diagnostic], value? : Datatype } ``` ## `validateAlgOrn` _validateAlgOrn: total predicate `{ ok, diagnostics }` over candidate `algOrn` args — checks each algebra arm against its description shape without throwing._ ``` validateAlgOrn : Attrs -> { ok : Bool, diagnostics : [Diagnostic] } ``` ## `validateFunctional` _validateFunctional: total predicate `{ ok, diagnostics }` over candidate functional-ornament `args` — `coreOf` is applied to `.ornament` first so generated datatypes pass through._ ``` validateFunctional : Attrs -> { ok : Bool, diagnostics : [Diagnostic] } ``` ## `validateFunctionalLaws` _validateFunctionalLaws: delegates to `H.validateFunctionalLaws` — total predicate `{ ok, diagnostics }` over a functional ornament's law-check bundle._ ``` validateFunctionalLaws : FunctionalOrnament -> { ok : Bool, diagnostics : [Diagnostic] } ``` ## `validateSpec` _validateSpec: total predicate `{ ok, diagnostics }` over an `(base, spec)` candidate for the user-facing `ornament` surface — never throws._ ``` validateSpec : DataSpec -> OrnamentSpec -> { ok : Bool, diagnostics : [Diagnostic] } ```