An open record type, parametrised by a row r with bare field values (f ~ Identity).

ref:note-consumer-facade

[ref:note-rep-memory-physics] A Record is a flat, contiguous array of fields. Its memory layout is a single pointer to a small array of payload slots, plus an erased constructor tag (which is always 0 for products).

An open record type, parametrised by a functor f and a row r.

ref:note-consumer-facade

[ref:note-rep-memory-physics] A RecordF is a flat, contiguous array of fields where each field slot contains a value wrapped in f.

An open variant type, parametrised by a sum row s with bare field values (f ~ Identity).

ref:note-consumer-facade

[ref:note-rep-memory-physics] A Variant is a single value that can be any one of the constructors defined in the sum row s. Its memory layout is exactly identical to a Record, except the tag distinguishes which constructor is currently active.

An open variant type, parametrised by a functor f and a sum row s.

ref:note-consumer-facade

[ref:note-rep-memory-physics] A VariantF is a single value that can be any one of the constructors defined in the sum row s, with each field slot wrapped in f.

A product row: an ordered list of field names and field types.

ref:note-rep-memory-physics

Order is the identity of the row; two rows with the same fields in a different order are different rows. This is deliberate — it is what lets a field index be a compile-time constant (0, 1, 2, ...) synthesized directly into Core by the polytropos-plugin without runtime linear scanning.

A sum row: an ordered list of constructor names, each carrying the product row of that constructor's fields.

ref:note-rep-memory-physics

The tag of a constructor is its 0-based position in this list. Constructor arities are therefore the lengths of the nested product rows, and may differ (see note §3, D7).

An HKD-aware product row parameterised by a field functor f.

In an HKD-aware product row, each field value is wrapped in the functor f. Since f ty has kind Type for any ty :: Type, this is an alias for a row where field types are parameterised by f.

A pattern synonym for matching and constructing variants safely.

ref:note-patterns-view-patterns

Pattern synonym for matching and constructing HKD variants safely.

ref:note-patterns-view-patterns

Construct an empty record.

The empty record has no fields and an arity of 0.

Construct an empty HKD record.

Insert a new field at the beginning of a record.

This extends the record's row type by prepending the new field. At runtime, this copies the underlying array and adds the new value.

Invariant: This function expects the type-level field list to match the runtime representation. Using it sequentially correctly builds up a record in standard layout format.

Insert a new field wrapped in f into an HKD record.

Inject a record of fields into a variant for a specific constructor.

Inject an HKD record into an HKD variant for a specific constructor.

Project a specific constructor from a variant.

Project an HKD record from an HKD variant.

Compute the payload product row of a constructor n in a sum row s.

Compute the HKD payload product row of a constructor n in an HKD sum row s.

Sub-row relationship between two product rows.

ref:note-subrow-subsum

[ref:note-subrow-subsum-mechanics] SubRow sub super holds when every field in sub occurs in super with the same field type. The plugin emits the 0-based projection slot indices as evidence.

Algorithmic Mechanics: For sub-record projection `projectRecord sub superRec`, the runtime must extract the subset of fields in sub from super. The subRowIndices method returns a precomputed permutation vector `[Int]` containing the exact slot indices in super@. This allows projection to execute in a single O(|sub|) pass with zero type search.

Sub-sum relationship between two sum rows (variant widening & narrowing).

ref:note-subrow-subsum

[ref:note-subrow-subsum-mechanics] SubSum sub super holds when every constructor in sub occurs in super with identical field rows. The plugin emits the injection tag indices (for widening) and narrowing tag indices (for projection) as evidence.

Algorithmic Mechanics: 1. Widening (widenVariant): Total and O(1). Every constructor in sub is present in super. The runtime tag t in sub is mapped to `subSumInjectIndices !! fromIntegral t`, which is precomputed by the plugin. 2. Narrowing (narrowVariant): Partial and O(1). Inspects `subSumNarrowIndices !! fromIntegral t`. If the constructor is present in sub, returns `Just subTag`; otherwise Nothing.

Project a sub-record from a super-record (bare).

Extracts only the fields present in sub in the order specified by sub.

ref:note-subtyping-combinators

[ref:note-subrow-subsum] [ref:note-subrow-subsum-mechanics] Complexity: \(\mathcal{O}(|sub|)\) array copy, with literal projection indices precomputed at compile-time by the Polytropos.Plugin.

let fullRec = REC { id = 1 :: Int, name = Alice, role = Admin }
    subRec  = projectRecord @'["name" ':= String] fullRec

Project a sub-record from a super-record (HKD).

Extracts only the fields present in sub in the order specified by sub.

ref:note-subtyping-combinators

[ref:note-subrow-subsum] [ref:note-subrow-subsum-mechanics] Algorithmic Mechanics: The TcPlugin statically proves that sub is a subset of super and emits the projection permutation vector subRowIndices sub super. At runtime, this function reads each slot from the source array and constructs a new flat array of size |sub| in a single linear pass.

Widen a variant from a sub-row to a super-row (bare).

ref:note-subtyping-combinators

[ref:note-subrow-subsum] [ref:note-subrow-subsum-mechanics] Widening is total and constant time (\(\mathcal{O}(1)\)): the active constructor tag in sub is remapped to its corresponding tag in super via a compile-time synthesized literal tag lookup table, requiring zero payload array allocations.

let smallVar = VAR { Ok = REC { val = 200 :: Int } } :: Variant '[Ok ':= '["val" ':= Int]]
    wideVar  = widenVariant @'[Ok ':= '["val" ':= Int], Err ':= '["msg" ':= String]] smallVar

Widen a variant from a sub-row to a super-row (HKD).

ref:note-subtyping-combinators

[ref:note-subrow-subsum] [ref:note-subrow-subsum-mechanics] Widening is total and constant time: the active constructor tag in sub is remapped to its corresponding tag in super, preserving payload slots.

Narrow a variant from a super-row to a sub-row (bare).

ref:note-subtyping-combinators

[ref:note-subrow-subsum] [ref:note-subrow-subsum-mechanics] Returns Just with the active tag remapped to sub if the active constructor belongs to sub, or Nothing if the constructor is not a member of sub.

Complexity: \(\mathcal{O}(1)\) time. Reuses the underlying payload array directly.

Narrow a variant from a super-row to a sub-row (HKD).

ref:note-subtyping-combinators

[ref:note-subrow-subsum] [ref:note-subrow-subsum-mechanics] Returns Just with the active tag remapped to sub if the constructor belongs to sub, or Nothing if the constructor is not in sub.

Peel a single constructor n from an open variant in \(\mathcal{O}(1)\) time.

ref:note-peeling-elimination

If the variant's active constructor is n, returns Right (Record fs). Otherwise, returns Left (Variant (Delete n s)) with the runtime tag decremented if \(t > target\) and preserved if \(t < target\), requiring zero heap reallocation or payload copying.

This is the core primitive enabling single-construct compiler passes (Nanopass):

desugarStmt :: Variant (While ':= fs ': CoreRow) -> Variant CoreRow
desugarStmt v = case peel @While v of
  Right (REC { cond, body }) -> desugarWhile cond body
  Left rest                  -> rest  -- O(1) pass-through for all other constructs!

Peel a constructor n from an open HKD variant in \(\mathcal{O}(1)\) time.

ref:note-peeling-elimination

Delete a constructor n from a sum row s.

Type-level subtraction for open variant rows, enabling type refinement during sequential peeling passes.

Row of handler functions for a sum row s returning a uniform result res.

Row of monadic handler functions for a sum row s returning m res.

Row of heterogeneous handler functions mapping constructors in s to results in resRow.

Row of heterogeneous monadic handler functions mapping constructors in s to monadic results in m (Record rfs).

Eliminate a closed variant uniformly with \(\mathcal{O}(1)\) array jump table dispatch.

ref:note-array-jump-table-elimination

Handlers are provided as a Record where each field corresponds to a constructor in s. The runtime reads the variant's tag \(t\) and directly indexes slot \(t\) of the handler array, executing without linear branch cascades.

let res = eliminateUniform handlers myVariant
  where
    handlers = REC
      { Ok  = \(REC { code, body }) -> "Status " ++ show code
      , Err = \(REC { reason })     -> "Error: " ++ reason
      }

Eliminate a closed variant uniformly inside a monad m with \(\mathcal{O}(1)\) array jump table dispatch.

ref:note-array-jump-table-elimination

Full hybrid eliminator: eliminate a closed variant into an open variant of per-constructor results.

ref:note-array-jump-table-elimination

Each handler in s transforms that constructor's payload into a corresponding result in resRow. The resulting variant retains the original constructor tag and payload in \(\mathcal{O}(1)\) time.

Full monadic hybrid eliminator: eliminate a closed variant into an open variant of per-constructor results inside m.

ref:note-array-jump-table-elimination

Syntactic synonym for eliminateUniform taking the variant value first.

ref:note-array-jump-table-elimination

Convenient for direct pattern matching expressions resembling Swift or Rust match:

matchVariant expr REC
  { lit = \(REC { val }) -> val
  , add = \(REC { left, right }) -> left + right
  }

A type-level pair: a name bound to a type.

Poly-kinded with independent parameters, mirroring large-anon's Pair / :=. Kept deliberately simple; the f-functor parameter that large-anon threads through its rows is future work (see note §1, D3).

Algorithmic Mechanics: In type expressions, ("name" ':= Type) provides an ergonomic, readable alternative to tuple pairs '("name", Type). Because := is an ordinary data constructor promoted by DataKinds, GHC treats it as a first-class type constructor of kind k1 -> k2 -> Type.

Field-wise equality for a product row.

The method works over RowRep, so the row is in the type and no Proxy argument is needed (obligation 4, design note §6). A plugin will build the body by substituting literal slot indices and a literal element count, so there is no type-level search at the use site.

ref:note-literal-evidence

The test suite writes these bodies by hand, which makes the tests the specification of what the plugin must emit.

Field-wise Show for a product row. See RowEq for the design.

ref:note-literal-evidence

The plugin synthesizes an unrolled sequence of per-field showsPrec calls, formatting each field label as a literal string "fieldname = " followed by the field value's showsPrec, joined by comma separators.

The class that abstracts over row flavours.

Each flavour has an associated EntryKind — the kind of a single entry in a row of that flavour. The plugin uses this to know what to inspect.

A zero-cost witness for a type-level field name.

Can be constructed ergonomically via OverloadedLabels (e.g. #foo).

Algorithmic Mechanics: Field has no runtime fields and is represented by GHC as a zero-cost singleton. When the user writes #foo, GHC desugars this to fromLabel "foo". The IsLabel instance below matches when the label string l unifies with the expected field symbol l'@, constructing Field at compile time with zero runtime allocation.

Evidence that every field in a row satisfies a class.

This is the generic dictionary-supply class the plugin solves for fully-known rows. Its evidence is a flat array of type-erased field dictionaries, in row order, so callers can map/fold over all fields without writing per-row instances by hand.

The class is kind-polymorphic in the row parameter so the same surface can be reused for the legacy Row rows and for the HKD-aware product and sum rows once those are layered on top. The row flavour parameter remains so the plugin can distinguish product vs sum rows.

The evidence type for AllFields: a flat array of type-erased per-field dictionaries, in row order.

Extract field names as a type-level list of Symbols.

For each field "name" ':= ty in the row, this evaluates to "name". When the row is fully known, the TcPlugin rewrites this type family to a concrete type-level list of symbols.

Extract field names and bare field types as a type-level list of pairs.

For each field "name" ':= ty in the row, this evaluates to '("name", ty). When the row is fully known, the TcPlugin rewrites this type family to a concrete type-level list of pairs.

Extract field names and instantiated field types as a type-level list of pairs.

For each field "name" ':= ty in the row, this evaluates to '("name", f ty). When the row is fully known, the TcPlugin rewrites this type family to a concrete type-level list of pairs.

Class providing a compile-time hash for a label Symbol.

The TcPlugin solves this by evaluating the hash (FNV-1a 64-bit) of the literal symbol at compile time and emitting a literal Word dictionary.

Purpose and Non-Purpose

• Purpose: KnownHash provides O(1) integer keys for dynamic/HAMT label dispatch, label interning, and name-based field lookup without requiring KnownSymbol dictionary plumbing or runtime string hashing in hot paths.

• Non-purpose: KnownHash is not used for slot offset indexing in records and sums. Record slot access in polytropos is statically determined at compile time by FieldIndex and ConstructorIndex (0, 1, 2, ...), which are dense, collision-free literal offsets into repVals.

Algorithmic Mechanics: The FNV-1a 64-bit algorithm evaluates over the UTF-8 bytes of the label string: hash = 14695981039346656037 (offset basis) for each byte c: hash = (hash xor c) * 1099511628211 (prime)

Ergonomic helper to extract the compile-time hash of a label via a proxy (such as Field or Proxy).

Synonymous with labelHash for compatibility with large-record conventions.

FNV-1a 64-bit hash of a String, matching the hash computed at compile-time by the TcPlugin for KnownHash.

Syntactic marker for anonymous record construction and pattern matching. Desugared by the Polytropos source plugin.

ref:note-source-plugin-arch

Syntactic marker for anonymous functorial/HKD record construction. Desugared by the Polytropos source plugin.

ref:note-source-plugin-arch

Syntactic marker for anonymous variant injection and pattern matching. Desugared by the Polytropos source plugin.

ref:note-source-plugin-arch

Syntactic alias for VAR.

Pattern synonym alias for VAR.

Marker for record update syntax: REC_UPD r { x = 42 }. Desugared by the Polytropos source plugin into setField calls.

ref:note-source-plugin-arch

[ref:note-view-patterns]

Marker for functorial/HKD record update syntax: REC_UPD_F r { x = Just 42 }. Desugared by the Polytropos source plugin into setFieldF calls.

ref:note-source-plugin-arch

[ref:note-view-patterns]

Marker class for open record declarations desugared by the source plugin.

ref:note-open-declarations

Marker class for open variant declarations desugared by the source plugin.

ref:note-open-declarations

Fetch a field value from a record, used for pattern matching and field access.

Algorithmic Mechanics: In view patterns emitted by the source plugin for pattern matching on records (REC { x, y }), field values are extracted using recordField. It queries GHC's built-in HasField constraint, which is solved by polytropos-plugin using the precomputed 0-based index of field n.

Update an existing field in a Record.

Algorithmic Mechanics: Resolves FieldIndex at compile time to obtain the literal slot index of n in r, coerces the new value to 'Identity Any', and delegates to setFieldAt.

Update an existing field in a RecordF.

Map a class-constrained function over all fields of a record.

Algorithmic Mechanics: 1. Fetches pre-resolved dictionary vector fieldDicts (a contiguous SmallArray of type-erased DictAny entries). 2. Clones the underlying payload array into a mutable SmallMutableArray in ST. 3. In a tight unrolled loop from 0 to N-1: - Fetches the dictionary at slot i and unpacks DictAny, bringing c Any into scope. - Fetches the payload at slot i, coerces to Any, and invokes f. - Writes the coerced result back into slot i in-place. 4. Freezes the mutable array into an immutable Record.

Complexity: Exactly 1 array allocation of size N, zero intermediate list allocations.

Fold over all fields of a record using a class constraint.

Algorithmic Mechanics: Recursively traverses the dictionary vector and payload array from index 0 to N-1. For each slot, unpacks DictAny, maps the value using f to a monoidal value m, and combines the results using <>.

Complexity: Zero heap array allocations.

Zip two records of identical row shape applying a class-constrained function.

Algorithmic Mechanics: Walks both records in parallel from slot 0 to N-1, applying the binary function f using the dictionary from fieldDicts, writing results into a newly allocated array.

Complexity: Exactly 1 array allocation of size N, zero intermediate list allocations.

Map a class-constrained function over all fields of an HKD record.

Fold over all fields of an HKD record using a class constraint.