VOLTAreference

Reference / Language and libraries

Define your own value types

Language and libraries

Open in the workbench →
On this page · 4 sections

For advanced authors: describe reusable kinds of values so functions and modules can communicate their intent more clearly.

What it is#

Name your own types and introduce your own constructors, then case on them. Type aliases, nominal records, sum types (enums and tagged unions with payloads), constructor patterns in case, and parameterized (generic) types. This is the floor under the rest of the "real language" cluster: it gives Chords, scales and harmony a first-class Chord value, Configurable library modules its typed config records, and the trait work its generics. Records are compile-time structure and constructors have compile-time tags; signal expressions inside them still lower to the audio graph. No runtime record allocation or runtime sum tag is introduced.

Surface#

-- type alias
type Beats = Int

-- nominal record
type Chord = { root: Pitch, quality: Quality, inversion: Int }
c = { root = ~C4, quality = Maj7, inversion = 0 }   -- construct
c2 = c with { root = ~D4 }                           -- functional update
r = c.root                                           -- field access

-- sum type: nullary constructors and payload-carrying constructors
type Quality      = Maj | Min | Dom7 | Min7 | Maj7 | Dim | Aug | Sus2 | Sus4
type Interval     = Chromatic Semitones | Diatonic Int
type Articulation = Staccato | Tenuto | Accent Normalized

-- constructor patterns in `case` — the arms are a braced, comma-separated
-- list (a payload binds a name)
accentGain = \a -> case a of {
  Staccato   -> 0.6,
  Tenuto     -> 0.8,
  Accent amt -> 0.8 + amt * 0.2        -- binds `amt`
}

-- parameterized (generic) type
type Option a = Some a | None
firstOr = \d xs -> case head xs of { Some x -> x, None -> d }

A Chord value is something you transform before it sounds — transpose / parallelMinor / invert are ordinary Chord -> Chord functions (no new builtins), and the chord lowers to its pitch set exactly as chord "c4" "maj7" does. Example song: examples/songs/changes.volta (a ii–V–I built by transforming one seed chord). Stdlib source: examples/songs/harmony.volta (Quality / Chord / Interval + the transform operators).

Records can be named, locally bound, returned from factories and passed intact to ordinary functions. Typed record parameters check missing, extra, duplicate and incompatible fields. Nested projection and with updates share these value rules; see Configurable library modules for configurable kits.

List Hz checks each element's unit. Constructor arguments instantiate generic payloads: Some 42 has type Option Int, while Some "hello" cannot satisfy an Option Int annotation. Known scrutinee arguments also type the variables bound by a constructor pattern. with updates change the result's field types; reading an updated seconds field cannot satisfy an Hz annotation. Unknown type names and incorrect type-application arity are errors.

Repeated occurrences of a generic parameter must agree through nested lists, tuples, records and callable signatures. Later occurrences can refine unknown parts of an earlier payload. Separate constructor calls have independent type arguments. A supplied generic constructor also retains its own parameter relationships: Box : a -> Box a cannot satisfy b -> b, because that would require an infinite type. The error belongs to the consuming argument, including when the constructor is imported or passed through an alias/container. Type aliases may refer forward to other aliases or records; their declaration order does not weaken checking. Cyclic aliases are errors; recursive sum types retain their nominal identity.

Generic callbacks also contribute evidence to a constructor's type arguments:

type Apply a b = Apply a (a -> b) | Empty
id = \x -> x
frequency = Apply 440Hz id   -- Apply Hz Hz
duration = Apply 2s id       -- Apply Seconds Seconds

The compiler checks the callback with the input type supplied by that call. Callbacks in records, tuples, lists and constructor payloads use the same constraints. Evidence from later arguments can refine earlier callbacks. Inline, named and returned callbacks retain their inferred results; a generic parameter does not replace the callback's body type. Known incompatible units and obligations on unused locals are errors even in unselected callback alternatives. Checking does not execute callbacks or draw musical randomness.

Open payloads stay open: an empty list can propagate List ? through an identity callback, but this does not prove its element type. Deliberate ?name holes retain their goals with the available contextual type. Excessive nesting, non-converging refinement and excessive inferred type size produce errors. Ordinary functions and constructor callbacks share lexical inference. Complete builtin descriptors and closure of all executable obligations remain in Language Foundations.

How it's implemented#

  • Compiler:
    • ast.rs — Decl::TypeDef, TyDefBody::Sum(Vec<Variant>), and CasePat::{Bind, Ctor} for constructor patterns.
    • parse.rs — parse_type_decl (aliases / records / sums), parse_case_pat (Ctor(name, subpatterns)).
    • check.rs — TypeEnv (alias map); constructors register as a value (nullary) or an Ty::Arrow (payload); Ty::Var identifies quantified declaration parameters and subst_vars instantiates type syntax.
    • check/inference/arena.rs — fresh inference handles, structural equations, occurs checks, bounded type reconstruction and rollback of failed equations. check/inference.rs instantiates constructor schemes independently and projects unsolved terms to the existing open-type boundary. Handles never enter the serialized type model or executable core.
    • check/inference/expressions.rs — lexical schemes, capture-aware generalization and retained operation/projection constraints. Constructor callbacks use the ordinary solver; the old callback refinement loop is removed. check/constructors.rs binds surface arguments and contextualizes deliberate holes. Quantified parameters are not authored annotations.
    • eval.rs — CtValue::Variant { type_name, ctor, args }; match_pattern recurses into Ctor payloads and binds Bind variables.
    • lower/pattern.rs — chord_from_record is the one compiler seam that turns a Chord record into its pitch set (mini.rs::chord_quality_offsets supplies the interval table).
  • Runtime: none — all user types are erased to compile-time CtValues; the IR and runtime never see a type tag.
  • Assets: the music ADTs ship in examples/songs/harmony.volta (synced into the browser's library by runtime/scripts/sync-assets.mjs).

Notes & limits#

  • Remaining foundations (Language Foundations P2.3–P2.6): complete overload descriptors and executable obligation closure. Known sum domains have exhaustive case checks, including domains established by inference. Pattern validation rejects unknown constructors, incorrect arity and incompatible scrutinee types before selecting an arm.
  • Types and constructors have module identity: a.Color and b.Color can coexist, and constructor patterns accept a.Red. Selective imports expose only the requested names; private types and their constructors stay private.
  • A statically known constructor may contain a live signal. case Pack m of { Pack x -> x, Empty -> 0 } extracts m without freezing it. A literal match against a live payload cannot select a static arm or skip to a fallback.
  • Planned/undecided directions — nominal vs structural equality, unit newtypes, term-level recursion — are Define your own value types §7 open questions, not shipped behavior.