Type-Level Rows in Turmeric

#row{Pos Vel}                 ; a positional row of two component types
#row{id : int  name : cstr}   ; a labeled row of two named columns

A row is not a value and never becomes one. It exists so that a type constructor can be parameterised by a set of types of arbitrary size -- "a query over Pos and Vel", "a table with an id and a name column" -- and have the compiler check that set the same way it checks any other type argument.

Rows are the mechanism behind tur-ecs's typed Query (see ecs-guide.md); this guide covers the underlying language feature.

Rows are not effect rows

Turmeric has two things called "rows", with two different kinds, two different reader forms, and no interaction between them:

When polymorphism-guide.md says "row polymorphism", it means the effect kind. This guide is about the type kind.

The kind [*]

Turmeric's kind system (see hkt-guide.md) normally deals in * and arrow kinds:

• * -- a plain type: int, Pos, Option<int>
• * -> * -- a unary type constructor: Option, Vec

A row adds one more sort of kind:

• [*] -- a row: a kind-level list of types

[*] is not *. A row cannot be used where a type is expected, and a type cannot be used where a row is expected. Both directions are kind errors, which is the whole point: (Query #row{Pos Vel}) is checked, not merely parsed.

Writing a row

Positional rows

Elements are ordinary type expressions, separated by whitespace. Compound types are fine:

#row{}                             ; the empty row
#row{int bool}
#row{Pos Vel Hp}
#row{(Option int) (Vec cstr)}

Every element must name a type that actually exists. An undeclared name is an error rather than a silently-invented placeholder -- this is what catches a typo'd component name in an ECS query:

error: unknown type name 'Velocityy' in #row{...} element position

A row holds at most 255 elements.

Labeled rows

A slot may instead be spelled name : type, giving a row of named fields:

#row{id : int  name : cstr}

Two labeled rows with identical element types but different names are distinct types and will not unify, so a Tbl #row{id : int} cannot be passed where a Tbl #row{name : int} is wanted.

Labels are all-or-nothing within a single literal. Mixing bare and labeled slots is TUR-E0290, and a repeated label is TUR-E0291:

#row{id : int  Foo}          ; TUR-E0290 -- typed-field literal needs `name : type` slots
#row{id : int  id : cstr}    ; TUR-E0291 -- duplicate field name `id`

Declaring a row-kinded parameter -- ^&

A type parameter marked ^& has kind [*] and accepts a row. It works on defstruct, deftype, defdata, defgadt, and defn:

(defstruct Query [^&reads ^&writes] (world :int))
(deftype   Frame [^&cols]           (Frame :int))
(defdata   Tagged [^&cols]          (Tagged :int))
(defgadt   QueryG [^&cols]          (QueryG : (QueryG #row{int})))
(defn      frame-id [^&r] [f : (Frame r)] : (Frame r) f)

The ^& is a declaration site marker only. Everywhere else -- field types, return annotations, call-site ascriptions -- you write the bare name (r, not ^&r).

At every application site the argument's kind is checked against the parameter's:

(defstruct Box   [a]   (v :int))   ; kind * parameter
(defstruct Query [^&r] (world :int))

(Box   #row{int bool})   ; TUR-E0012 -- parameter 1 expects kind '*', argument has kind '[*]'
(Query int)              ; TUR-E0012 -- parameter 1 expects kind '[*]'

Under-application is allowed, as with any type constructor: given two row parameters, (Query #row{Pos}) is a partially applied constructor of kind [*] -> *, not an arity error.

Where a row may appear

A row may appear only as a type argument to a ^& parameter. It is not a value, and it is not a type a value can have:

(def r #row{int bool})
;; error: #row{...} is a type-level row and can only appear in a type
;; annotation, not as a value expression

(defn f [x : #row{int bool}] : int 5)
;; error [TUR-E0012]: `#row{...}` is a type-level row (kind [*]); a value
;; cannot have row type

The second check is applied at every nested position of a value type, so a row hidden inside an arrow argument is rejected the same way.

The row algebra

Four type-level operations combine rows. Each is written in type position and produces a row usable anywhere a literal row is:

All four preserve a labeled row's field names; see Labels through the algebra for the rules that follow from that.

row-concat / row-union / row-intersect are variadic: zero operands give the empty row, one operand passes through. Every operand must itself be a row; a non-row operand is an error:

error: 'row-union' operand 2 must be a #row{...} (kind [*]), got a non-row type

A worked union -- joining two component sets, with Pos deduplicated:

(defopaque Pos :int)
(defopaque Vel :int)
(defopaque Hp  :int)

(defstruct Query [^&comps] (world :int))

(defn join [w : int] : (Query (row-union #row{Pos Vel} #row{Pos Hp}))
  (:: (make-struct Query w) (Query #row{Pos Vel Hp})))

(defn run [q : (Query #row{Pos Vel Hp})] : int
  (.world q))

(defn main [] : int
  (println (run (join 7)))
  0)

Row equality -- order matters, row-canon opts out

Two rows are equal when they have the same elements in the same order. #row{int bool} and #row{bool int} are different types.

This is a deliberate default: it keeps ordinary type_eq a cheap positional walk, and it means a row can encode an ordered thing (a column list, an argument order) as well as an unordered one.

When you want permutation-insensitivity, ask for it explicitly with row-canon, which sorts the row into a canonical order. Two callers who both canonicalise agree regardless of how they spelled the row:

(defstruct Frame [^&cols] (n :int))

(defn make-ab [n : int] : (Frame (row-canon #row{int bool}))
  (:: (make-struct Frame n) (Frame (row-canon #row{int bool}))))

(defn make-ba [n : int] : (Frame (row-canon #row{bool int}))
  (:: (make-struct Frame n) (Frame (row-canon #row{bool int}))))

(defn use-canon [f : (Frame (row-canon #row{int bool}))] : int (.n f))

(defn main [] : int
  (println (use-canon (make-ab 1)))
  (println (use-canon (make-ba 2)))
  0)

The relaxation is scoped to the annotations that opt in. type_eq itself is never weakened, so a module that does not write row-canon keeps strict order-sensitive equality.

Labels through the algebra

Every operation forwards a labeled row's field names, so a label survives the round trip and keeps doing its job -- (row-canon #row{id : int}) stays distinct from (row-canon #row{name : int}).

Two rules follow from labels being part of a slot's identity:

Labeled rows dedup and intersect on the (name, type) pair. row-union collapses two slots only when they agree on both, and row-intersect keeps a slot only when both sides label it the same:

(row-union     #row{id : int} #row{id : int})     ;; => #row{id : int}     (one slot)
(row-intersect #row{id : int} #row{name : int})   ;; => #row{}             (labels differ)

row-canon sorts labeled rows by (field_name, type_name), with the field name leading -- otherwise #row{a : int b : int} and #row{b : int a : int} would compare equal at every slot on type alone and keep their two different input orders.

Labels are all-or-nothing across an operation, the same rule the literal enforces. Mixing a labeled operand with a bare one is TUR-E0290:

(row-union #row{id : int} #row{int})
;; error: 'row-union' operand 2 mixes a labeled row with a bare one; labels are
;; all-or-nothing across the whole operation (TUR-E0290)

The empty row is the exception, because it contributes no slots to disagree about: (row-union R #row{}) is the identity whether or not R is labeled.

A labeled fold can also reach a state no literal could spell -- row-concat keeps duplicates outright, and row-union keeps two slots that share a name but disagree on type. Either way the result carries a repeated field name, which is TUR-E0291:

(row-concat #row{id : int} #row{id : int})
;; error: 'row-concat' result has duplicate field name `id` (TUR-E0291)

Rows are erased

Row arguments are phantom. They participate in type checking and in name mangling, and then they are gone -- a struct with two row parameters emits a C struct holding only its real fields:

typedef struct tur_adt_Query {
    int64_t world;
} tur_adt_Query;

So the checking is free at runtime. There is no row descriptor, no reflection over a row, and nothing to pay for at a call boundary. It also means a row can never be inspected at runtime: if you need the component list as data, you must build that data yourself alongside the type.

Worked example -- an ECS system's read and write sets

The motivating use. A Query carries two independent rows, so a system's signature states exactly which components it reads and which it writes:

(defopaque Pos :int)
(defopaque Vel :int)

(defstruct Query [^&reads ^&writes] (world :int))

(defn integrate [w : int] : (Query #row{Pos Vel} #row{Pos})
  (:: (make-struct Query w) (Query #row{Pos Vel} #row{Pos})))

(defn run-system [q : (Query #row{Pos Vel} #row{Pos})] : int
  (.world q))

(defn main [] : int
  (println (run-system (integrate 11)))
  0)