Skip to content

Design

Jump to bottom
joshsh edited this page Jul 19, 2026 · 11 revisions

Design rationale

This page records deliberate design decisions in Hydra — the "why we chose this, and not the obvious alternative" behind aspects of the language that a reader might reasonably second-guess.

It is distinct from Concepts, which describes the model as it is. This page answers why. When a choice here is settled, the relevant Concepts/section links to it rather than repeating the justification inline.

Entries are settled decisions, not open questions. In-flight design exploration belongs in GitHub issues; once a decision is made and stable, summarize the rationale here and link the issue.

Inheriting JSON syntax for printing and parsing conventions

Where a Hydra surface form has a JSON counterpart, Hydra inherits the JSON syntax rather than defining its own variant, and the corresponding kernel primitives are the JSON serializers.

Instances:

  • Strings: parseString/printString implement RFC 8259 string syntax exactly — one escape production shared by the JSON wire format, the textual syntax's string literals, and its backtick-quoted names.
  • Decimal numbers: parseDecimal accepts RFC 8259's number grammar (scale-preserving: 1.10 and 1.1 are distinct values); printDecimal is representation-faithful, laying out the preserved coefficient digits with ECMAScript Number::toString (§6.1.6.1.20) / RFC 8785 (JCS) thresholds and spellings. The JSON coder calls these primitives directly for number input/output.
  • Floats: the shortest-round-trip digit rule and the non-finite sentinel spellings (NaN, Infinity, -Infinity, -0.0) are shared between the JSON wire format and the textual syntax.
  • Binary: base64 (standard alphabet, padded) in both the wire format and textual literals.

Why: JSON is the only other language with built-in hydra-kernel support, so deferring to it means one specification and one implementation per convention, with byte-level agreement between the wire format and the textual syntax by construction — there is no second normalization layer that could drift. Where JSON's grammar is poorer than Hydra's (non-finite floats, distinguishing literal precision), Hydra adds the minimum on top (sentinel tokens, :width suffixes) without altering the inherited part.

Decision ratified 2026-07-19 (#579 textual-syntax finalization and the #417 S5 primitive pins); stated normatively in docs/specification/ (index conventions; instances in syntax.md §2).

Ordered map keys

Hydra requires the key type of a map to be orderable. This is a deliberate design choice, not an inherited limitation: every term in Hydra — including a map term — needs a canonical representation that survives translation into any target language. A total order on keys gives a map a single canonical form (a deterministic key/value sequence) that every host reproduces identically, regardless of how that host implements maps internally.

In practice this excludes almost nothing. Hydra terms have a canonical order for all first-order shapes, so the only key types ruled out are those with no canonical identity at all — chiefly functions, which are excluded for a stronger reason than non-orderability: function equality is undecidable, so a function couldn't serve as a key even in an unordered (hash-based) map.

Two alternatives are sometimes raised — keys ordered by a supplied ordering function (rather than a natural order on the type), or merely-hashable keys paired with a hashing function. Both are perfectly constructible in Hydra today (e.g. a list of key/value pairs plus an ordering or hashing function), but neither is a fundamental constructor in the language, because the natural-order map already provides the canonical, translation-stable representation Hydra needs.

Discussion: issue #230.

Union introduction as inject

The constructor that builds a value of a union type (selecting one variant and supplying its payload) is called inject. This is standard typed-lambda-calculus terminology: inject is the introduction form for a sum type, dual to project (the elimination form for a product/record). Alternatives like variant or construct are sometimes proposed, but inject/project is the established, symmetric pair and is kept deliberately.

Annotations as a separate type and term variant

Hydra makes annotated a distinct variant of Type and Term (a record pairing an inner type/term with an annotation Term/Type carrying its metadata), rather than baking metadata fields into every variant or carrying a parallel metadata map alongside each module.

The annotation field is typed as Term (resp. Type) since #386; the canonical encoding for what host code thinks of as a Map<Name, Term> is a TermMap keyed by TermVariables, bridged by the kernel helpers wrapAnnotationMap and getAnnotationMap. Treating the annotation slot as a Term rather than a fixed Map<Name, Term> lets specialised users substitute a different representation (e.g. a list of pairs, an injection into a richer ADT) without re-shaping every annotated node.

This choice has three load-bearing consequences:

  • Stacking. Multiple annotation layers can be applied to the same inner type or term by nesting annotated nodes; tools that need to reason about a particular annotation key can peel layers from the outside without worrying about which inner type or term they apply to.
  • Small grammar. Every non-annotation variant has exactly the fields its semantic role requires. Adding a new annotation key never modifies the grammar of Type or Term — it just goes into the annotation Term of an enclosing annotated node.
  • Easy traversal of the unannotated core. A traversal that doesn't care about metadata can call a single helper (kernel Annotations.deannotateType / …Term) once at the top and then walk the variants directly. The alternative — fields-on- every-variant — would require every traversal to ignore those fields explicitly, multiplied across every host.

The accepted cost is the "peel through annotations" step that consumers of the annotated form have to perform; in practice this is one helper call per traversal and is mechanical.

Granularity: whole terms and types only

Annotations attach only to whole Term and Type nodes — the annotated constructors are the only place annotations occur in the grammar. No other construct (record fields, union variants, lambda binders, let bindings, type parameters) carries an annotation slot. To annotate one of those, wrap the enclosing term or type in an annotated node.

The question of whether to relax this — adding optional annotation fields to Lambda, Field, Binding, and friends — was examined in depth on issue #215 and decided against, on three grounds:

  1. Demand. A census of every annotation actually written across all Hydra packages found that finer-grained annotation is used for exactly one thing: documentation — field descriptions (by convention, wrapping the field's type) and definition descriptions (wrapping the definition's term). The use cases that per-construct slots would uniquely enable — metadata on a specific lambda binder or inner let binding that survives into generated code — had zero consumers.

  2. Cost. Because the affected constructs are records, adding even optional slots is a breaking change at every positional construction site (on the order of 140 sites across the kernel, before counting generated hosts), touches each of the kernel's structural-recursion spines, and adds dead weight to every future induction over Term/Type in proof assistants (#326).

  3. The second channel. The deepest objection: Hydra's whole annotation discipline — inference transparency (infer the body, re-attach the annotation), the deannotate / strip helpers, and every traversal that "peels through" metadata — is built around the single annotated constructor. Annotation slots on other constructs would constitute a second metadata channel invisible to all of that machinery: strip functions would not strip it, transparency rules would not cover it, and every consumer would have to know about both channels.

The positive half of the decision is a relocation: documentation metadata belongs at the definition layer, not on type and term expressions at all. The packaging model's EntityMetadata (descriptions, comments, cross-references, lifecycle) attaches to packages, modules, and definitions, keyed by exactly the names that authors write and code generators emit — the same resolution Javadoc reaches with @param living in the method's doc block rather than on an AST parameter node. Annotations remain the vehicle for what they are good at: domain-specific, application-defined metadata riding a type or term expression (field-name preservation hints, wire-format keys, type hints).

For the historical arc, see the original decision against core annotation slots ("a significant complexity add and a further departure from System F") and the reframing comment that redirected the underlying need toward definition-layer metadata, which the issue continues to track.

Why Hydra does not support row polymorphism

Hydra deliberately omits row polymorphism — row variables, structural record/union types, record extension and restriction, and open (polymorphic) variants. The decision was made against the implementation as it exists, and the full analysis is recorded on issue #328 (decision and analysis in one comment, a deferred escape-hatch specification in the next).

Three grounds, in brief:

  1. Demand. Every motivating use case — schema migration (#327), property-graph and algebraic-graph mappings, open metadata, partial updates, generic record programming — is served by a mechanism Hydra already has, usually more generally. Chief among them: Hydra's types are first-class data, so row operations (extend, restrict, rename, diff, merge) are ordinary total functions over list<FieldType>, and generated coercion terms are re-checked by the kernel's own inference. The row variable's job — "copy the rest, whatever it is" — is done by the metaprogram, which always holds the closed field list.

  2. Cost. Hydra's labeled types are nominal by construction: every record and union term carries a schema name, and structural forms exist only where all nine targets share a universal representation (pairs, eithers, lists). Rows would add new term syntax, rewrite unification (today pure textbook Robinson), extend the elaboration contract past System F, and have no single representable form on nominal targets such as Java, Scala, and Python.

  3. Precedent. Every language in Hydra's class — nominal, multi-target, inference-centric — declined rows (GHC, ending at the HasField constraint after twenty years), retreated (Elm removed field extension/deletion in 0.16, citing zero observed usage), or marginalized them (OCaml). Rows thrive only where the language is structural-first and every target represents records freely (PureScript), or in restricted, evidence-erased form (SML#).

Sanctioned substitutes: meta-level row operations over list<FieldType> with per-instance re-checking (the stated foundation for #327's TypeDiff), and — if generic field access ever earns its keep — a deferred, fully speced hasField constraint riding the existing TypeScheme.constraints vehicle: no row variables, no unification changes, no kind system. See the #328 hatch specification.

Scope note: the decision covers rows over data records and variants. Effect typing is a separate question: Hydra's effect type is currently a single blanket constructor, and any future proposal for labeled effect sets (where rows are the standard technology, cf. Koka) must be evaluated on its own merits.

Why collection types are built in

Hydra's collection types — lists, maps, sets, optionals, pairs, eithers, and unit — are dedicated structural variants of Type and Term, not applications of type constructors: list<string> is a TypeList node, not an application node List @ string. This design was reaffirmed in 2026 against the mature implementation, and the full investigation — a census of every special-casing site, the alternatives considered, and the staged path forward — is recorded on issue #87 (see the closing comments).

Three grounds, in brief:

  1. The structural form pays its way. That "being a list type" is a syntactic fact is exactly what lets adapters classify and rewrite unsupported collections per target language (e.g. lowering optional values to 0-or-1-element lists), coders map each collection to a native container, and the JSON wire format stay compact. The census found the duplication cost of the special casing modest and concentrated (on the order of 400 lines in inference plus checking, small per-coder encode arms), while the machinery that depends on cheap syntactic classification is a feature, not an accident.

  2. Generalize capability, not representation. What the structural form cannot express — abstracting over the container itself, as in unifying m a with list<int32> — is planned to come from a solver-internal spine normal form (#226), in which the built-in constructors behave as nominal constants during unification while the structural variants remain the canonical at-rest representation. This changes no wire format and no generated code; it adds capability inside the type solver only.

  3. Classes as data, not new kernel forms. Functor/monad-style generality is delivered through instance records (#581) whose members are ordinary top-level polymorphic definitions, rather than through new term forms; do-notation was considered and rejected (analysis on issue #87). Relatedly, universally quantified record fields are rejected by design — see the "all types are inferrable" principle on Concepts — so an "instance" is a bundle of named polymorphic definitions, not a record carrying rank-2 fields.

Scope note: monadic effects are a separate question from monadic structure: Hydra's kernel has no effect monad (the former Flow type was removed in favor of the abstract effect<> type constructor and the hydra.lib.effects primitives — see Effects), and nothing in the collection-type decision constrains future effect typing.

Coders bundle encode and decode

A Coder in Hydra pairs an encoder (source → target) with a decoder (target → source) in a single value, rather than letting them be authored as two independent functions. Alternatives are common — many serialization stacks ship an encoder and a decoder as separate modules, sometimes from different authors.

The bundled form is preferred for three reasons:

  • Round-trip identity is a single-source claim. When an author writes a Coder, they are simultaneously asserting the pair is consistent. Round-trip tests are then a property of the Coder rather than a cross-module coincidence: decoding the result of encoding a value should yield the original (modulo a documented lossiness flag).
  • One Coder per format pair. A reader who wants to know how Hydra exchanges with Avro looks at one place, not two. Format-pair-specific invariants (which fields encode where, how nominal types map, what's lossless and what isn't) live together with the code that enforces them.
  • Coder composition is closed. Two Coders composing into a third (Avro ↔ Hydra ↔ Protobuf, for instance) is well-defined because each side is itself bidirectional. A composition of two unidirectional encoders would give you a one-way Avro → Protobuf path with no symmetric way home.

The accepted cost is that authoring a Coder is harder than authoring an encoder alone — the author has to think about the inverse direction even when only one is immediately needed. In practice this cost is paid once per format, not per use.

Adapters as the type-aware layer above Coders

A Coder transforms values between two representations that already share a type schema. An Adapter adds the type-level half: source and target types, a Coder over those types' values, and an isLossy flag. The two frameworks are deliberately kept separate.

The rationale:

  • Value-level transformations don't always need a type-level mapping. Within a single type system, encode/decode is purely value-level; folding type-level fields into every Coder would burden the simpler case.
  • Cross-language coding inherently needs both. Adapting a Hydra record into a Java class involves two different type-level objects bound together with a value-level Coder and a lossiness claim. The Adapter is where both halves meet.
  • Composition has different rules at each level. Coders compose pointwise (Avro ↔ Hydra ↔ Protobuf at the value level). Adapters compose more carefully — both type-level mappings must compose, and the combined lossiness flag is the disjunction of the pair's.

The accepted cost is one more abstraction to learn before writing a cross-language coder.

Coders per target language

Each target language has its own coder, packaged separately: hydra-java, hydra-python, hydra-scala, hydra-lisp, hydra-typescript, hydra-go, hydra-coq, hydra-wasm. There is no global "all targets" coder.

This mirrors the modular package structure already chosen for everything else in Hydra. A change to one coder is bounded to that coder's package and its downstream consumers, not the universe of every coder Hydra knows how to emit. A new target language is added by writing one new coder package, not by extending a central registry. The set of supported target languages can be discovered by listing the coder packages, rather than by inspecting a hardcoded list in a central module.

The per-language packaging also lets Hydra's composability principle operate at the package level: coders compose. The build orchestration in bin/sync.sh is one application — piping Hydra modules through the JSON coder (in hydra-kernel) and then through the per-target coders — but the per-language coder packages are also independently usable by downstream applications that want to compose them with their own coders.

Topological-sort emission

Hydra emits code in topological-sort order over the module-dependency DAG: each target module appears in the output stream only after every module it depends on. This is host-agnostic: Haskell and Java tolerate forward references via the build system, but Lisp dialects, certain Python flavors, and WASM-style emission don't, so topo-sort is the granularity that works in every host Hydra targets.

The downstream consequence is that emission can stream — a host's coder processes one module at a time and never has to look ahead, since every name the current module mentions is either already defined or is a known primitive.

Explicit Either (and Maybe) error handling

Hydra's kernel surfaces failures through explicit return types. Operations that produce a value on success return Either SomeError a; checks that only report a finding return Maybe a, where a is the finding type (e.g. Maybe InvalidTermError to mean "either there is an invalidity to report or there isn't"). The concrete result and error types vary by subsystem. The kernel does not use exceptions, monad-transformer stacks, Result<T, E>-style sugar, or any language-specific error-handling idiom.

The reason is translingual portability. The kernel runs in every host Hydra targets, and the error mechanism has to translate cleanly into all of them with no host-specific runtime support.

  • Exceptions are host-divergent. Each host has its own model (checked vs unchecked, condition restarts in Lisp, panics in Go, etc.) and what catches what depends on the host's call-stack semantics.
  • Monad stacks have no portable representation. A StateT (ExceptT Error) is meaningful in Haskell and unfaithful elsewhere; not every host has Applicative/Monad as a type-level abstraction.
  • Result<T, E> is syntactic sugar over the same sum. Hydra's Either is the language-neutral form; per-host coders render it as Result / Either / Maybe / Option / tagged union as appropriate.

Subsystems that need threaded state — notably inference, via InferenceContext — pass it as an explicit parameter rather than concealing it in a monad. The accepted cost is verbosity at every call site; the gain is a single error-handling pattern that the entire kernel and every coder share.

Host interaction follows the same discipline: rather than impure primitives or a host-specific IO monad, Hydra makes effects explicit in the type via the effect<t> type constructor, with recoverable failures still expressed as either<e, t>. See Effects for the effect model and the standard effect libraries.

Module-level dependencies

Each Hydra module carries a dependencies field — the set of other modules it references. Module-level dependency information is used by:

  • Incremental sync. The dirty-set closure walks reverse dependency edges: when a module's source changes, every module that depends on it (transitively) must be re-inferred.
  • Per-host code emission. Each coder consumes the dependency set to generate the host's import / use / require statements at the top of every emitted file.

Both consumers run at sync time. Without persisted module-level dependency information, each consumer would have to scan every module's term and type bodies — an O(n · m) walk per consumer per emission, where n is the number of definitions in the module and m is the average size of a definition's term-or-type tree. With the field, that scan happens once per module and is amortized against every later read.

The same caching argument applies as for inference: term and type analyses are expensive, and we persist the results in the JSON layer rather than recomputing them at every consumer.

Derivation of the field is tracked in #419.

Clone this wiki locally