Skip to content

Validation

Jump to bottom
Joshua Shinavier edited this page Jul 10, 2026 · 1 revision

Validation

Audience: readers who want to understand Hydra's validation framework — the check/finding/verdict model, the full catalog of constraints it enforces, and how it fits into the sync pipeline.

What validation does

Hydra validation follows a check → finding → verdict model. A check inspects one piece of structure (a term node, a type node, a module, a package, a property-graph element) and produces a finding: Maybe SomeError describing what was observed, or Nothing if nothing is wrong. A check never decides on its own whether that finding matters — that decision belongs to a ValidationProfile, which classifies each check's rule as a hard error, a warning, or leaves it unevaluated altogether.

This separation is what lets the same check serve different callers. A team building a strict CI gate and a team building an interactive linter can point the same check at two different profiles and get two different verdicts, without the check itself changing.

All validation is translingual. Every check is authored once, in the Haskell DSL under packages/, and generated into every host language. The same rule, with the same qualified name and the same semantics, runs in Haskell, Java, Python, Scala, TypeScript, and the Lisp dialects. A Haskell caller and a Python caller validating the same term or the same graph get identical verdicts, because they are running the same generated logic — not two independent reimplementations that happen to agree today. This is the whole point of building validation as a Hydra package rather than as host-specific glue: verdicts are guaranteed identical by construction, not by convention.

The framework types — hydra.validation

Source: Hydra/Sources/Kernel/Types/Validation.hs.

ValidationProfile is a record with four fields:

  • errorRules: Set Name — the fully qualified rule names whose findings are treated as errors.
  • warningRules: Set Name — the fully qualified rule names whose findings are treated as warnings.
  • maxErrors: int32 — hard upper bound on collected errors; the traversal stops as soon as this many errors have been collected.
  • maxWarnings: int32 — soft upper bound on collected warnings; once reached, further warning matches are silently dropped, but the traversal is not terminated by this.

A rule's fully qualified name has the form hydra.error.<package>.<UnionType>.<variant>, for example hydra.error.core.InvalidTermError.duplicateBinding. A rule whose name is in neither errorRules nor warningRules is silently skipped — its check function is never even evaluated for that profile. Setting maxErrors = 1 reproduces the legacy "first error wins" behavior that Hydra used before profiles existed.

ValidationResult e is a record with two fields, both lists of the finding-payload type e:

  • errors — findings classified as errors, in traversal order, bounded by maxErrors.
  • warnings — findings classified as warnings, in traversal order, bounded by maxWarnings.

A validation pass is successful exactly when errors is empty; warnings are informational and never affect that judgment.

Module-naming convention

Validation constraint modules use the hydra.validate.* namespace — for example hydra.validate.core, hydra.validate.packaging, hydra.validate.pg, hydra.validate.neo4j. This is distinct from hydra.validation, which is reserved for the framework types themselves (ValidationProfile, ValidationResult).

Constraint reference

hydra-kernel

hydra.validate.core — term and type validation

Source: Hydra/Sources/Kernel/Terms/Validate/Core.hs.

This module walks the term tree (via term) and the type tree (via type_), checking one node at a time and threading a ValidationResult accumulator through the recursion. Term checks run in either untyped or typed mode; typed mode additionally activates a set of System-F-specific checks (undefined type variables in binding types, lambda domains, and type applications).

Term rules:

Rule What it enforces
emptyTermAnnotation A TermAnnotated annotation map must be non-empty.
nestedTermAnnotation A TermAnnotated body must not itself be TermAnnotated.
constantCondition logic.ifElse must not be applied to a literal boolean.
selfApplication A variable must not be applied to itself.
unnecessaryIdentityApplication The identity lambda (\x -> x) must not be applied.
redundantWrapUnwrap unwrap(n) must not be applied to wrap(n, _).
emptyTypeNameInTerm Record/inject/project/cases/wrap must carry a non-empty type name.
duplicateField Record fields and case alternatives must have unique names.
emptyLetBindings A let must have at least one binding.
duplicateBinding Let bindings must have unique names.
invalidLetBindingName A let binding name must be non-empty.
undefinedTypeVariableInBindingType Typed mode: a binding's type scheme references no unbound type variable.
termVariableShadowing A lambda parameter must not shadow a graph-bound name.
invalidLambdaParameterName A lambda parameter name must be non-empty.
undefinedTypeVariableInLambdaDomain Typed mode: a lambda's domain references no unbound type variable.
undefinedTypeVariableInTypeApplication Typed mode: a type application references no unbound type variable.
typeVariableShadowingInTypeLambda A type-lambda parameter must not shadow an in-scope type variable.
invalidTypeLambdaParameterName A type-lambda parameter name must be non-empty.
emptyCaseStatement A case statement must have at least one case or a default.
undefinedTermVariable A variable reference must resolve to a bound term, a lambda variable, or a primitive.

Type rules:

Rule What it enforces
emptyTypeAnnotation A TypeAnnotated annotation map must be non-empty.
nestedTypeAnnotation A TypeAnnotated body must not itself be TypeAnnotated.
voidInNonBottomPosition TypeVoid is only allowed in bottom positions.
typeVariableShadowingInForall A forall parameter must not shadow a bound type variable.
invalidForallParameterName A forall parameter name must be non-empty.
nonComparableMapKeyType A map key type must not be a function type.
nonComparableSetElementType A set element type must not be a function type.
emptyRecordType A record type must have at least one field.
duplicateRecordTypeFieldNames Record type field names must be unique.
emptyUnionType A union type must have at least one field.
singleVariantUnion A union has exactly one variant (classified as a warning in the default profile).
duplicateUnionTypeFieldNames Union type field names must be unique.
undefinedTypeVariable A type variable must be bound in the current scope.

The default profile, kernelDefaultCoreProfile, classifies every rule above as an error except singleVariantUnion, which is a warning — single-variant unions are sometimes a deliberate design choice (an extensible variant kept as a union from the start so a second variant is a non-breaking addition later). maxErrors = 1, maxWarnings = 20.

hydra.validate.packaging — module and package validation

Source: Hydra/Sources/Kernel/Terms/Validate/Packaging.hs.

Module-level checks:

Rule What it enforces
conflictingVariantName For each union type, the generated constructor name (capitalize(type) ++ capitalize(field)) must not collide with another type's local name in the same module.
missingDocumentation Every top-level definition must carry a non-empty description annotation at its outermost layer.
invalidDefinitionName Term/primitive local names match camelCase; type local names match PascalCase (^[A-Z][a-zA-Z0-9]*$, no underscores).
definitionNotInModuleName Every definition name must have the module's namespace as a dotted prefix.
definitionsOutOfOrder The module's definitions list must be sorted ascending by local name. Hand-written Source modules only — generator-derived modules (hydra.dsl.*, hydra.encode.*, hydra.decode.*) use semantic grouping instead and are exempt.
duplicateDefinitionName Definition names must be unique within a module.
invalidModuleNameConvention The module namespace matches the dotted-lowercase namespace regex.

Package-level checks:

Rule What it enforces
conflictingModuleName No two module namespaces may be identical when lowercased (a case-insensitive filesystem collision).
duplicateModuleName Module namespaces must be unique within a package.
invalidPackageName The package name matches the hyphen-lowercase regex.

Cross-universe check — the fatal gate introduced by #574:

Rule What it enforces
undeclaredDependency Every free name a module references (term free variables plus nominal type references; type-definition structural references) whose owner is known must be either the module itself or one of its directly declared moduleDependencies. This is one-hop, stricter than transitive resolution: a module must directly declare the dependency that owns any name it references, even if that name is also transitively reachable through some other declared dependency. Primitives are excluded. Every violation in a module is accumulated, not just the first.

The default profile, kernelDefaultPackagingProfile, classifies all seven module rules and all three package rules as errors, with no warnings; maxErrors = 1, maxWarnings = 20. It deliberately excludes undeclaredDependency, which is universe-scoped (a referenced name's owner can live in a different package than the referencing module) and is run separately from the per-package profile machinery.

Per-package profile dispatch (#575)

hydra-kernel is held to kernelDefaultPackagingProfile — every module and package rule above is a hard error, with zero exemptions. Every other package is validated under kernelPackagingProfileWithDocWarnings, which is identical to the kernel profile except that three rules are downgraded from error to warning: missingDocumentation, definitionsOutOfOrder, and invalidDefinitionName.

This exists because re-enabling comprehensive packaging validation surfaced large, pre-existing backlogs of documentation, ordering, and naming-convention violations scattered across many hand-written DSL source files outside the kernel — not concentrated in one or two files, but spread thin enough that fixing them wasn't a quick pass. Downgrading those three rules to warnings for non-kernel packages lets /sync proceed while each package's backlog is remediated incrementally (tracked in #580); as a package's backlog clears, its call site moves from the warnings profile to the fully-fatal kernel profile.

The dispatch itself, packagingProfileFor in Hydra.Generation, is an interim mechanism: a hardcoded list of package names (strictPackagingPackages, currently just hydra-kernel) checked with elem. The intended long-term design is a typed PackageValidationConfiguration declared per package in package.json (see #512), so that a package's validation strictness is data it owns rather than a list maintained in the generator.

hydra-pg

hydra.validate.pg — property-graph validation

Source: Hydra/Sources/Validate/Pg.hs.

Function What it does
validateVertex Checks a vertex's label against its VertexType, its id against the caller-supplied checkValue, and its property map via validateProperties.
validateEdge Checks an edge's label, id, and property map the same way, plus outVertexNotFound/outVertexLabel and inVertexNotFound/inVertexLabel — the out/in-vertex ids resolve and their labels match the EdgeType's expected endpoints. These endpoint checks only fire when the caller supplies a vertex resolver.
validateProperties Three rules over a property map against its schema: missingRequired (a required key is present), unexpectedKey (every actual key is declared in the schema), invalidValue (a schema-known key's value passes the caller's checkValue).
validateGraph Orchestrates the above: validates every vertex, then every edge, lifting per-element findings into InvalidGraphError.

defaultPgProfile classifies every PG rule as an error, with no warnings; maxErrors = 1, maxWarnings = 20.

See the Property graphs wiki page for the PG data model these checks validate against, and the ValidatePG demo (source: ValidatePg/Demo.hs) for a worked, translingual example — the same generated validator runs against the same JSON fixtures in Haskell, Java, and Python, with identical verdicts by construction.

hydra.validate.neo4j — Neo4j property-graph validation

Source: Hydra/Sources/Validate/Neo4j.hs. This validator is pure and client-side: it checks only what is determinable from the data it is handed, performs no effects, and never queries a database.

Function What it does
validateNode Matches a node against every NodeElementType whose identifying label the node carries, then checks: noSuchLabel (the node matches no element type — closed-world, excluded from the default open-world profile), missingImpliedLabel (an implied label is absent), missingProperty and wrongPropertyType (per property constraint), and the cross-element constraints keyViolation and uniquenessViolation.
validateRelationship Matches candidate element types by relationship type, then by endpoint label pattern, then checks: noSuchType (closed-world, excluded by default), noMatchingPattern (the type has candidates but no candidate's start/end-label pattern matches), missingProperty and wrongPropertyType, endpoint existence (startNodeNotFound/endNodeNotFound), and the cross-element keyViolation/uniquenessViolation.
validateGraph Orchestrates node and relationship validation over a whole graph, resolving relationship endpoint labels from the node list.

The cross-element constraints (keyViolation, uniquenessViolation) and the endpoint-existence checks (startNodeNotFound, endNodeNotFound) are first-class, intended parts of the Neo4j validation spec — their error variants are already defined in hydra.error.neo4j and their rule names are already registered in the rule-name catalog that the profiles draw from.

Two profiles are provided: defaultNeo4jProfile (open-world — the closed-world noSuchLabel and noSuchType rules are excluded, so an element matching no schema type is valid by default) and strictNeo4jProfile (closed-world — those two rules are also errors). Both use maxErrors = 1, maxWarnings = 20.

See the Neo4j validation demo (source: Neo4jValidation/JsonDemo.hs) for a worked, translingual example: the same generated validator runs against shared JSON fixtures in every host, so a Cypher-derived graph produces identical verdicts everywhere.

Profiles

Profile Domain Errors Warnings Excluded maxErrors maxWarnings
kernelDefaultCoreProfile Term/type validation All core rules except singleVariantUnion singleVariantUnion — 1 20
kernelDefaultPackagingProfile Module/package validation (hydra-kernel) All 7 module rules + 3 package rules — undeclaredDependency (run separately) 1 20
kernelPackagingProfileWithDocWarnings Module/package validation (non-kernel packages) Same rules minus the 3 below missingDocumentation, definitionsOutOfOrder, invalidDefinitionName undeclaredDependency 1 10000
defaultPgProfile Property-graph validation All PG rules — — 1 20
defaultNeo4jProfile Neo4j validation (open-world) All rules except closed-world — noSuchLabel, noSuchType 1 20
strictNeo4jProfile Neo4j validation (closed-world) All rules including closed-world — — 1 20

Where validation runs

Packaging validation and core term/type validation are enforced as part of code generation: a package's structure and a module's term/type trees are checked while dist/json/** and the downstream host distributions are generated, not as a separate, optional linting pass. The undeclared-dependency check (#574) was the first fatal gate wired into that flow — a module referencing a name whose owner isn't among its declared dependencies stops generation outright, at the point where the incident that motivated the check (a symbol moving to a module in another package without the referencing module's dependency list being updated) would otherwise have gone undetected. The per-package structural/semantic packaging checks described above (#575) are wired alongside it, with the kernel-strict / non-kernel-relaxed profile split described earlier.

For where these checks sit in the pipeline's phase structure and cache model, see build-system.md. For how and when to run the validator as part of a maintenance pass, see maintenance.md. This page covers what the framework is and which constraints exist, not the operational how-to.

Cross-references

Clone this wiki locally