Std.Generic

Generic representation building blocks for user-extensible derives. See docs/planning/user-extensible-derives.md.

Types

U1

type U1 =
  | U1

The unit shape — represents zero fields / a nullary constructor.

Leaf

type Leaf a =
  | Leaf a

A single field, holding a value of type a.

Labeled

type Labeled (n : Symbol) a =
  | Labeled a

A named field. The name lives at the type level as a Symbol-kinded parameter — library impls recover the string via KnownSymbol.

And

type And l r =
  | And l r

A product (two-or-more fields are right-leaning chains of And).

Or

type Or l r =
  | Or_Left l
  | Or_Right r

A sum (two-or-more variants are right-leaning chains of Or).

Variant

type Variant (n : Symbol) a =
  | Variant a

A sum constructor. The constructor name lives at the type level as a Symbol-kinded parameter — library impls recover the string via KnownSymbol. Distinguishes constructor labels from record-field labels (Labeled).

Record

type Record a =
  | Record String a

Top-level framing wrapper for records: runtime type name + inner shape. Gives library codecs a hook for outer framing (e.g. JSON object braces).

Adt

type Adt a =
  | Adt String a

Top-level framing wrapper for ADTs: runtime type name + variant tree. Gives library codecs a hook for outer framing distinct from records.

Traits

Generic

trait Generic a r {
  fun to : a -> r
  fun from : r -> a
}

Isomorphism between a user type a and its structural representation r. The first parameter functionally determines the second (coherence rule).