Design

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.

---

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.