Containers, Polynomial Functors, and Ornaments

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

A list of length three contains three elements. Its description code in chapter 80 records how the list is constructed, but it does not isolate the choice “length three” from the three places where elements occur. Make that separation first. Take the natural number $3$ as the shape and $\mathsf{Fin}(3)$ as its set of positions. A list over a type $X$ is then a pair $$(n,f):\sum _{n:\mathbb{N}}\mathsf{Fin}(n)\to X.$$ The function $f$ fills every position of the chosen shape with an element of $X$. This factorization is semantic: it tells us which choices determine the layout and which choices merely fill that layout.

Shapes and positions

The list container is $$C_{\mathsf{List}}:=(\mathbb{N},\lambda n.\mathsf{Fin}(n)).$$ The element $(3,\lambda i.\mathsf{lookup}(xs,i))$ represents a three-element list $xs$. The empty shape has no positions: $$⟨C_{\mathsf{List}}⟩X\ni (\mathsf{0},\lambda i.{\mathsf{rec}}_{\mathbf{0}}(i)).$$ Here $i:\mathsf{Fin}(0)$, so empty elimination defines the contents map. The shape is not the stored data. Replacing $X$ by another type changes the possible contents but leaves $\mathbb{N}$ and every $\mathsf{Fin}(n)$ fixed.

For the list shape $3$, the map with $h(n)=n+10$ calculates as $${\mathsf{cmap}}_{C_{\mathsf{List}}}(\lambda n.n+10,(3,[2,4,8]))\equiv (3,[12,14,18]).$$ Only the position labels have been abbreviated by list notation; the calculation is pointwise application to $\mathsf{Fin}(3)$.

Proof of Proposition 81.3 — Container action laws

Proof. Write $u\equiv (s,h)$. The first components on both sides are $s$. At a position $p:P(s)$, the two contents calculations are respectively $$h(p)=h(p),g(f(h(p)))=g(f(h(p))).$$ Sigma congruence with these pointwise paths gives the two stated equalities. ◻

Maps that preserve layouts

A polymorphic layout transformation cannot inspect an $X$-element. It may choose a target shape from the source shape, then say where each target position obtains its source element. The direction of that second map is the first important variance calculation in the chapter.

The position map runs from target positions to source positions because a target contents request must be answered from the given source contents. A map in the other direction could discard source positions, but it would not say how to fill a newly created target position.

Reverse on length-indexed lists is the morphism $$m_S(n):=n,m_P(n,i):=n-1-i$$ with truncated natural subtraction interpreted inside $\mathsf{Fin}(n)$. At shape $3$, $$⟨m{⟩}_X((3,[x_0,x_1,x_2]))\equiv (3,[x_2,x_1,x_0]).$$ This is the calculation used by Abbott, Altenkirch, and Ghani when they introduce container morphisms [AAG05].

The laws follow by beta computation. More importantly, extension respects composition. For $u\equiv (s,f)$, The source paper proves that, in its extensional setting, container morphisms correspond fully and faithfully to natural transformations between container extensions. We use only the displayed direction: a container morphism gives the polymorphic map $⟨m{⟩}_X$. The converse requires the source’s extensional equality and parametric/naturality interface; it is not a theorem of $T_0$ merely because the two types look alike.

Polynomial operations

Containers calculate like polynomials because a shape chooses a monomial and its positions count occurrences of the variable. This is an equation about extensions, not permission to use subtraction or division on arbitrary types.

For the product, a value has a shape pair and a contents map on a coproduct of positions. Splitting that map gives one $C$-contents map and one $D$-contents map: The equivalence sends $h$ to its restrictions along $\mathsf{inl}$ and $\mathsf{inr}$; the inverse performs case analysis. The sum calculation instead yields $$⟨C+D⟩X\simeq ⟨C⟩X+⟨D⟩X.$$

A composite shape first chooses an outer shape $s$, then one inner shape at each outer position. A composite position chooses an outer position $p$ and then an inner position in $k(p)$. Reassociating Sigma types gives $$⟨C\circ D⟩X\simeq ⟨C⟩(⟨D⟩X).$$ For binary trees, composing the one-layer container with itself distinguishes the outer branching choice from the branching choices at its children. A single flattened count would lose that tree shape.

Algebras and coalgebras under explicit hypotheses

The expression $F(X)=1+A\times X$ has many fixed points. Finite lists and possibly infinite lists are selected by universal properties, not by the equation $X\simeq F(X)$ alone.

Proof of Theorem 81.9 — Conditional fold and unfold laws

Proof. The first equation is exactly the commuting condition for the unique algebra morphism from the initial algebra to $(A,\alpha )$. The second is the commuting condition for the unique coalgebra morphism from $(A,\gamma )$ to the final coalgebra. Existence and uniqueness are hypotheses in the two universal properties; this proof does not construct W-types or M-types. ◻

For $C_A$ representing $1+A\times X$, an assumed initial algebra gives finite lists and its fold equation. An assumed final coalgebra gives possibly infinite lists and its unfold equation. These are different selections of a solution to the same shape-position equation.

Indexed containers

A vector layer must know both the index of each recursive child and the index of the result. A unary container has only one ambient type $X$, so it cannot record this flow of indices.

For vector layers over $A$, take $I=J=\mathbb{N}$. At result index $0$, there is one nil shape with no recursive positions. At result index $\mathsf{suc}(k)$, a cons shape stores an $A$-element, has one recursive position, and sends that position to $k$. Its extension therefore calculates to $$⟨C_{\mathsf{Vec}(A)}⟩X(0)\simeq \mathbf{1},⟨C_{\mathsf{Vec}(A)}⟩X(\mathsf{suc}(k))\simeq A\times X(k).$$ These are the two fibers of the vector description in chapter 80; they have been interpreted semantically, not identified definitionally with the description code.

The indexed source proves initiality of its indexed W-type construction and a normal-form result for strictly positive families. Proposition 5.2 gives the initial algebra calculation, including the commuting square and uniqueness proof, while the final comparison records that the reduction to W-types uses extensional propositional equality [AGH^+15]. We therefore import only the following bounded statement.

Proof of Theorem 81.12 — Indexed-container representation, source signature

Imported proof. This imported theorem does not turn every endofamily operator into a container. It applies only to the source grammar and assumptions, and it does not transfer initiality or finality to the syntactic description universe of chapter 80 without an interpretation theorem. The imported construction and its initiality calculation are Proposition 5.2 and the normal-form development on pp. 24 and 39 of [AGH^+15]. ◻

Derivatives are one-hole contexts

Consider a product $X\times X$. Removing one occurrence of $X$ leaves either a hole on the left with one stored right element, or a hole on the right with one stored left element. Thus its one-hole contexts have type $X+X$. The ordinary derivative $\partial (X^2)=2X$ predicts the same two cases.

Proof of Proposition 81.14 — Plugging one hole

Proof. The constant case has empty domain. For $X$, the unique context is $\star$ and ${\mathsf{plug}}_X(\star ,x):=x$. A sum context remembers its injection and uses the induction hypothesis in that branch. A product context is either $$\mathsf{inl}(c,g):(\partial F(X))\times G(X)\text{or}\mathsf{inr}(f,d):F(X)\times \partial G(X).$$ Define $${\mathsf{plug}}_{F\times G}(\mathsf{inl}(c,g),x):=({\mathsf{plug}}_F(c,x),g),$$ and define the right case by $(f,{\mathsf{plug}}_G(d,x))$. These clauses cover the regular grammar. ◻

The list equation $L(X)=1+A\times X$ describes one layer, while a complete list is its least fixed point. A one-hole context in a complete list is a prefix and a suffix: the hole is the focused element between them. For $[a,b,c]$ focused at $b$, use $$([a],[c]).$$ Plugging $b^{\prime }$ gives $[a,b^{\prime },c]$. McBride derives this regular calculation directly [McB01]; the later container theory proves the sum, product, and chain laws for decidable containers [AAGM03].

Proof of Theorem 81.15 — Derivative laws at the decidable-container boundary

Imported proof. The decidability hypothesis selects the distinguished position needed by the container derivative. Dropping it does not leave the published construction available. The theorem asserts equivalences in the stated container setting; it does not define negative polynomial operations on arbitrary types. The displayed laws are the sum, product, and chain laws on pp. 12–13 of [AAGM03]. ◻

Ornaments refine structure

Vectors do not merely pair lists with a length proof. Their constructors carry exactly the index information forced by list length. The relation is directed: a vector forgets to a list, while an arbitrary list does not become a vector at a preselected length.

Cartesian layer transformations can insert stored Sigma data, delete data determined by a refined index, and refine recursive indices. These are constructions of ornaments, not permissions that replace the definition. The semantic presentation is the cartesian-morphism characterization of the description-ornament grammar of Dagand and McBride [DM14]; it is not arbitrary subtyping.

Take the natural-number description $1+X$. Inserting an $A$-element at every successor gives lists over $A$; forgetting all inserted elements gives list length. Algebraically ornament that list description by its length algebra. The fiber at $n$ is $\mathsf{Vec}(A,n)$, and the forgetful map is $${\mathsf{forget}}_{\mathsf{Vec}}:\mathsf{Vec}(A,n)\to \mathsf{List}(A).$$

For the list-length algebra this gives the vector fiber. The source construction replaces the redundant pair “list plus proof of length” by a constructor-indexed representation, but retains the coherence theorem [DM14]: $$\mathsf{length}({\mathsf{forget}}_{\mathsf{Vec}}(xs))=n(xs:\mathsf{Vec}(A,n)).$$

Proof of Proposition 81.18 — Transported map coherence

Proof. Induct on $xs$. At $\mathsf{vnil}$, both sides compute to $\mathsf{nil}$. In the successor case, write $xs\equiv \mathsf{vcons}(a,ys)$. The induction hypothesis gives $${\mathsf{forget}}_{\mathsf{Vec}}(\mathsf{vmap}(f,ys))=\mathsf{map}(f,{\mathsf{forget}}_{\mathsf{Vec}}(ys)).$$ Apply congruence for $\mathsf{cons}(f(a),-)$:  ◻

The proof transports one program and its defining equation from lists to vectors. It does not state that every list program has a unique lifting. Functional ornaments determine a coherence relation for a selected lifting; the remaining proof obligations depend on that function ornament [DM14].

What survives in ML

Dependent indices are not required to generate useful lifted code, but without them the index law moves out of the type and into a relation. Williams and Rémy’s ML example relates Peano naturals to lists by The relation is many-valued because the list head $a:A$ is new data. Their lift of addition therefore needs a patch telling the generated successor case where to obtain the head. After that patch, the generated term is list append [WR18].

Proof of Proposition 81.19 — The append lifting preserves the ML ornament

Proof. Induct on the witness of ${\mathcal{R}}_A(m,xs)$. In the zero/nil case, both $0+n$ and $\mathsf{append}(\mathsf{nil},ys)$ compute to the second input, so the second relation witness is the result. In the successor/cons case, write $m\equiv \mathsf{suc}(k)$ and $xs\equiv \mathsf{cons}(a,zs)$. The induction hypothesis gives $${\mathcal{R}}_A(k+n,\mathsf{append}(zs,ys)).$$ Applying the successor/cons clause yields $${\mathcal{R}}_A(\mathsf{suc}(k+n),\mathsf{cons}(a,\mathsf{append}(zs,ys))),$$ which is the goal after the defining equations for addition and append. ◻

The source lifting pipeline first abstracts the original ML term to a generic term, instantiates that term at the requested ornament relation, performs meta-reduction, and simplifies the result. Theorem 7.6 proves correctness only when the instruction is appropriate in the source judgment; at the strictly positive first-order instance, its logical relation specializes to the proposition above [WR18]. This is not the dependent vector theorem: ordinary ML accepts lists of every length, and the relation rather than the type carries the length invariant.

Bibliographic note

The shape-position presentation and its morphisms follow the container development of Abbott, Altenkirch, and Ghani and its expanded treatment with McBride [AAG05]. Indexed containers and their W/M-type boundary are taken from the 2015 journal development [AGH^+15]. The derivative calculation follows the primary container papers and McBride’s regular one-hole account [AAGM03, McB01]. The list/vector refinement and transport boundary follow Dagand and McBride [DM14]. The separate ML lifting comparison follows Williams and Rémy [WR18].

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 81.9, exercise 81.12.

Exercise 81.9¶

★★☆ For the list container, compose reverse with itself using definition 81.5. Calculate both components of the composite and prove that its extension at every $X$ is pointwise equal to the identity.

Referenced from 4 locations

• Containers, Polynomial Functors, and Ornaments
• ch:containers-ornaments: ch:containers-ornaments

Exercise 81.10¶

★★★ Calculate $\partial ((1+A\times X)\times (1+B\times X))$. Interpret every summand as a one-hole context and write the complete plugging function. Give one input for each summand.

Referenced from 3 locations

• Containers, Polynomial Functors, and Ornaments
• ch:containers-ornaments: ch:containers-ornaments

Exercise 81.11¶

★★☆ Build a two-element example showing that the equation $X\simeq 1+A\times X$ does not by itself select finite lists. Then name the exact universal property that distinguishes the finite solution from a final coalgebra solution.

Referenced from 3 locations

• Containers, Polynomial Functors, and Ornaments
• ch:containers-ornaments: ch:containers-ornaments

Exercise 81.12¶

★★★ Practical project.container-ornament-calculator Implement in Kappa the finite list container at shapes at most four, its reverse container morphism, the list-to-vector forgetful calculation, and a one-hole list zipper. Maintain the invariant that every contents array has exactly as many entries as its shape and that plugging increases the stored prefix-plus-suffix size by one. On the named input $[2,4,8]$, print the shape, the reversed contents, the result of replacing the focused value $4$ by $5$, and the forgotten vector contents. Reject a mutated vector with declared length $2$ and three elements with the witness shape-content-mismatch. The acceptance test passes exactly when the four calculations and the rejection witness match these values.

Referenced from 5 locations

• Containers, Polynomial Functors, and Ornaments
• Object calculus checker and evaluator
• ch:containers-ornaments: ch:containers-ornaments