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] }