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.

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.

A poly-kinded row whose entries have kind k.

Poly-kinded over entry kind k, mirroring large-anon's Row k. A row is represented purely as a standard type-level list [Pair Symbol k].

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.

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.

Synonym for ProductRow.

A poly-kinded sum row whose constructor payloads have product kind prod.

Sum rows map constructor name symbols to their payload specification.

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 sum row parameterised by a field functor f. Each constructor carries an HKD product row.

Synonym for SumRowHKD.

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.

The kind of row flavours (Option D).

Promoted by DataKinds: the types ProductRowT, SumRowT, HandlerRowT, ResultRowT have kind RowType, and can be used as the row parameter of RowRep and the evidence classes.

Algorithmic Mechanics: Option D uses concrete, distinct types for each row flavour rather than an open kind-polymorphic family. This allows the TcPlugin to immediately determine whether it is solving for a product row, sum row, HKD variant, or handler vector by inspecting the promoted type constructor, avoiding ambiguity and complex kind unification steps during constraint solving.

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 handler type: "handler for constructor n, with field types fs, returning result type res in monad m".

This is the entry kind of HandlerRowT. Each handler entry carries the constructor name, field types, result type, and monad explicitly, so that handler rows are self-contained and can be passed around without a paired sum row (see PHASE2_SKETCH.md, refinement #2).

A result type: "result for constructor n, of type res".

This is the entry kind of ResultRowT. Each result entry carries the constructor name and the result type.

Generic representation of a product or a sum.

ref:note-rep-memory-physics

The layout is exactly the one proposed for this project: a tag plus a flat array of payload slots.

newtype Rep f a = Rep (Word#, SmallArray# (f Any))

written here at the Haskell level, which has the same layout: {-# UNPACK #-} !Word is Word#, and SmallArray (f Any) is a SmallArray# (f Any) behind a newtype. SmallArray rather than Vector because it stores one pointer per element instead of a three-word box, which is the change large-generics 0.2 made for the same reason.

f is the functor applied to each payload slot, so that Rep I is isomorphic to the value itself and Rep Maybe boxes the slots.

Constructor index. 0 for a product.

For sums, this identifies which constructor of the sum row is currently active.

Payload slots, in row order, of the selected constructor.

For products, this contains all fields of the record. For sums, this contains only the payload fields of the active constructor.

Ephemeral mutable representation for in-place construction and deserialization.

ref:note-transient-cow

Allows O(1) in-place slot modification during multi-field updates, bulk parsing, or database row decoding without allocating intermediate immutable SmallArray wrappers.

Safely thaw an immutable Rep into a mutable builder.

Performs a single heap allocation of a SmallMutableArray and copies the N pointers from the source array.

Safely thaw a sub-slice of an immutable Rep into a mutable builder.

Safely freeze an ephemeral builder into an immutable Rep.

Uses unsafeFreezeSmallArray, which is an O(1) zero-copy operation that reuses the mutable buffer directly as an immutable SmallArray. Safe because caller relinquishes all mutable references in the enclosing ST action.

In-place slot write (O(1), zero allocation).

In-place batch slot writes (O(K), zero allocations).

Batch copy of a slice of fields from an immutable Rep into an MRep.

Uses hardware-accelerated memory block transfer (copySmallArray).

In-place batch block copy between mutable builders.

Allocate a new mutable MRep pre-initialized with a default payload.

Used when building a record or variant from scratch in ST before freezing.

Scoped pure modification wrapper.

Safely thaws an immutable Rep, runs an ST-scoped mutation callback, and freezes the result back into an immutable Rep without exposing mutable state.

Typed, row-carrying wrapper around Rep.

f is the functor applied to each payload slot. r is the row flavour (one of ProductRowT, SumRowT, etc.). row is the actual row data (a type-level list of entries), of any kind. a is the value type.

At runtime this is exactly Rep f a — a newtype with zero cost.

ref:note-rep-memory-physics

Zero-Cost Newtype Erasure: GHC's Core compiler completely unwraps RowRep at compile time. At runtime, all operations on RowRep compile down to direct primitive instructions on the underlying Rep. The type arguments r and row act as purely type-level evidence tags, allowing typeclasses like RowEq, RowShow, and AllFields to be invoked directly on records without requiring explicit runtime proxies.

Extract the underlying Rep from a RowRep.

Build a product from its field values, in row order.

ref:note-rep-memory-physics

The tag is 0: a product is the one-constructor sum. The payload values are placed directly into a contiguous SmallArray.

Build a sum value carrying the given tag and that constructor's fields.

ref:note-rep-memory-physics

The tag t is an unboxed integer identifying the active constructor. The payload array contains exactly the fields required by constructor t.

How many payload slots the selected constructor has.

Read the payload slot at a compile-time-known index.

The x is not determined by the index alone; it comes from the row type. The coercion is unchecked, exactly as in large-anon: the index is only ever produced by the plugin from a row that actually has that field.

Algorithmic Mechanics: In Core, this lowers directly to indexSmallArray# followed by a no-op cast. Because index i is a compile-time constant emitted by the TcPlugin, there is zero runtime dictionary lookup, zero branch instructions, and zero heap allocation.

Replace the payload slot at a compile-time-known index.

ref:note-transient-cow

For records with >32 fields (Milestone T3), uses hardware-vectorized SIMD non-overlapping block copies (copySmallArray), eliminating redundant reads and writes of slot i from the source array.

For small records (<=32 fields), uses direct in-cache thawSmallArray.

Clone once, apply K updates in-place, freeze once.

ref:note-transient-cow

Reduces multi-field update overhead from K * O(N) to 1 * O(N). For records with >32 fields (Milestone T3), sorts update offsets and copies non-overlapping unchanged slices in contiguous vectorized blocks.

Partial field update for sum constructors.

Ensures the runtime tag matches the expected constructor tag before updating. If the sum value is not currently the specified constructor, returns Nothing.

Project a constructor, or Nothing if the tag does not match.

A sum over a superset of the row can therefore be narrowed, but only observably: the failure is a Nothing, not a type error. See note §3, D8 for why widening is total and narrowing is not.

Eliminate a sum: hand the tag and the selected payload to a continuation.

The continuation sees the tag, so the unmatched case is the continuation's own business; this primitive does not decide it. The elimination story is unsettled — see note §4.

Peel a target tag from a sum representation in \(\mathcal{O}(1)\) time.

ref:note-peeling-elimination

If repTag r == targetTag, returns Right (toListSlots (repVals r)). Otherwise, returns Left r' where the remaining tag is preserved if repTag r < targetTag, or decremented by 1 if repTag r > targetTag.

Complexity: \(\mathcal{O}(1)\) time, requiring zero array payload copying or allocations.

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.

Field-wise equality for a sum row.

Sums need their own class because the comparison includes the tag (the constructor index), which products don't have (their tag is always 0 and folds away).

ref:note-literal-evidence

Algorithmic Mechanics: Two variant values v1 and v2 are equal iff: 1. Their runtime tags match: `repTag v1 == repTag v2` 2. Their payload fields for that specific active constructor match. The plugin emits a Core `case` expression on the tag, branching into per-constructor literal slot equality comparisons.

Field-wise Show for a sum row.

ref:note-literal-evidence

The plugin generates a jump table on repTag, emitting the constructor name as a string literal followed by its payload record's field representations.

Evidence that a field name or type n has a slot at a known index in a row.

The plugin solves this by inspecting the row and emitting the index as a literal (obligation 1, design note §5).

Algorithmic Mechanics: When GHC encounters a wanted constraint `FieldIndex "foo" r a`, the plugin scans the type-level list r for the entry `"foo" ':= a`. It returns the 0-based integer offset directly as a Core literal `Lit (MachInt i)`.

Evidence that a constructor name or type n has a known tag in a row.

The plugin solves this by inspecting the row and emitting the tag as a literal (obligation 2, design note §5).

Algorithmic Mechanics: For wanted `ConstructorIndex Bar s`, the plugin locates `Bar` in the sum row s and produces an unboxed integer literal `Lit (MachWord t)`.

Witness for a class constraint c a.

Standard GADT representation of an explicit typeclass dictionary.

Evidence that all fields of a row satisfy some class.

DictAny c is the type-erased form of c Any, mirroring large-anon's dictionary packing. It is what lets one dictionary carry many field dictionaries without a type-level list of them.

Algorithmic Mechanics: Under the hood, GHC typeclass dictionaries are ordinary record values containing function pointers (vtable). Because all boxed heap objects have identical runtime representation (a pointer), a dictionary for `c a` can be coerced to `c Any` via noInlineUnsafeCo. At point of consumption, passing an Any value cast from a to a method in `c Any` is completely type-safe because the vtable functions match the actual runtime type of the value.

Wrap a class dictionary into DictAny.

Construct evidence for the AllFields class.

Takes a list of type-erased dictionaries and places them into a contiguous SmallArray for O(1) indexed lookup during generic loops.

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.

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.

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.

A stand-in proxy for the row flavour. This is used in the smoke test as a placeholder for the row-flavour parameter of AllFields until the row vocabulary is finalised and the class is re-indexed.

The row-flavour proxy for product rows, used in the smoke test.

The row-flavour proxy for sum rows, for use in the smoke test once sum rows are exercised.

The row-flavour proxy for HKD product rows.

The row-flavour proxy for HKD sum rows.

unsafeCoerce that survives GHC's Core linter.

Must be marked NOINLINE: large-anon found that without it, GHC 9.6 produces -dcore-lint errors for the evidence built on top of this.

Algorithmic Mechanics & Compiler Safety Invariant: In modern GHC (9.6 through 9.14+), the Core simplifier performs aggressive inlining and floating of coercions. If an unchecked coercion is marked inlineable, GHC's simplifier may attempt to float the cast outside of enclosing lambdas or push it across case branches where the type invariants are not yet established. When running with -dcore-lint, this causes fatal Core Lint failures. Marking noInlineUnsafeCo as {-# NOINLINE #-} establishes an impenetrable optimization barrier, preventing the simplifier from inspecting or hoisting the underlying unsafeCoerce# primitive while still emitting zero runtime instructions.