Mendler Recursion, Nested Datatypes, and Mixed Variance

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

For an ordinary fixed point $\mu F$, a fold first maps its recursive function over one $F$-layer and then applies an algebra. That recipe assumes a map operation for $F$. It fails twice in the developments of this chapter. A nested datatype changes its parameter at a recursive occurrence, so one endofunctor $F:{\mathcal{U}}_i\to {\mathcal{U}}_i$ is not enough. A mixed-variance operator may place its argument to the left of an arrow, so it has no covariant map at all. Mendler’s repair does not give the recursive layer a map. It gives the algebra a polymorphic recursive-call argument whose abstract domain prevents the algebra from applying recursion to a value it has constructed itself.

The recursive call is abstract

First freeze the rank-zero interface. Let $F:{\mathcal{U}}_i\to {\mathcal{U}}_i$ be a type operator and assume a carrier ${\mu }^{\mathsf{M}}F:{\mathcal{U}}_i$ with constructor $${\mathsf{in}}_F^{\mathsf{M}}:F({\mu }^{\mathsf{M}}F)\to {\mu }^{\mathsf{M}}F.$$ This is a selected Mendler fixed-point interface, not the ordinary strictly positive fixed point of chapter 80. No destructor is available.

The complete interface appears in the fixed order formation, introduction, elimination, computation:

$\mathrm{\Gamma }⊢F:{\mathcal{U}}_i\to {\mathcal{U}}_i$

$\mathrm{\Gamma }⊢{\mu }^{\mathsf{M}}F:{\mathcal{U}}_i$

$\mathrm{\Gamma }⊢u:F({\mu }^{\mathsf{M}}F)$

$\mathrm{\Gamma }⊢{\mathsf{in}}_F^{\mathsf{M}}(u):{\mu }^{\mathsf{M}}F$

$\mathrm{\Gamma }⊢A:{\mathcal{U}}_i$$\mathrm{\Gamma }⊢\varphi :\prod _{R:{\mathcal{U}}_i}(R\to A)\to F(R)\to A$

$\mathrm{\Gamma }⊢{\mathsf{mfold}}_F(\varphi ):{\mu }^{\mathsf{M}}F\to A$

$\mathrm{\Gamma }⊢\varphi :\prod _{R:{\mathcal{U}}_i}(R\to A)\to F(R)\to A$$\mathrm{\Gamma }⊢u:F({\mu }^{\mathsf{M}}F)$

${\mathsf{mfold}}_F(\varphi )({\mathsf{in}}_F^{\mathsf{M}}(u))\equiv \varphi ({\mu }^{\mathsf{M}}F,{\mathsf{mfold}}_F(\varphi ),u):A$

The interface deliberately contains no positivity premise and no $F$-action. Its normalization claim is therefore not inherited from the strictly positive fixed points of chapter 80; it is the selected metatheorem stated below.

No ${\mathsf{map}}_F$ occurs in (84.1). This is the first gain: the algebra itself decides where its $R$-values occur. The universal quantifier is the second gain. A definition of $\varphi$ must work for every $R$, so it cannot assume $R={\mu }^{\mathsf{M}}F$, inspect an $R$-value, or pass a freshly constructed ${\mu }^{\mathsf{M}}F$ value to the recursive call $R\to A$.

For the list base operator $$F_A(R):=\mathbf{1}+(A\times R),$$ define Then

Proof of Proposition 84.3 — Ordinary folds are Mendler folds

Proof. For arbitrary $R$, the action sends $u:F(R)$ and $\mathit{rec}:R\to A$ to ${\mathsf{map}}_F(\mathit{rec},u):F(A)$. Applying $\alpha$ gives $A$. Substitution in (84.1) yields $${\mathsf{mfold}}_F({\varphi }_{\alpha })({\mathsf{in}}_F^{\mathsf{M}}(u))\equiv \alpha ({\mathsf{map}}_F({\mathsf{mfold}}_F({\varphi }_{\alpha }),u)),$$ the ordinary fold equation. ◻

The converse does not hold for an arbitrary $F$: a Mendler algebra can use the known constructors of $F(R)$ without supplying a map for all functions $R\to R^{\prime }$. This is why the presentation remains meaningful at selected mixed-variance operators.

Why the abstraction blocks self-application

If negative recursive occurrences are admitted together with an unrestricted destructor, termination fails without any value-level recursive definition. Consider the equations $$T\simeq (T\to \mathbf{1}),\mathsf{C}:(T\to \mathbf{1})\to T,\mathsf{out}:T\to (T\to \mathbf{1}).$$ Define $w(x):=\mathsf{out}(x)(x)$ and $\omega :=\mathsf{C}(w)$. Then $$w(\omega )\stackrel{\mathsf{out}(\mathsf{C}(w))\equiv w}{⟶}w(\omega ).$$ The cycle is generated by the negative occurrence of $T$ in $T\to \mathbf{1}$.

Now retain only the Mendler constructor for $F_{\mathsf{T}}(R):=R\to \mathbf{1}$. To recover the destructor, one would need a Mendler algebra with result ${\mu }^{\mathsf{M}}{F}_{\mathsf{T}}\to \mathbf{1}$: $$\varphi :\prod _{R:{\mathcal{U}}_i}(R\to ({\mu }^{\mathsf{M}}{F}_{\mathsf{T}}\to \mathbf{1}))\to (R\to \mathbf{1})\to ({\mu }^{\mathsf{M}}{F}_{\mathsf{T}}\to \mathbf{1}).$$ Given $f:R\to \mathbf{1}$, the attempted clause returns $f$. Its required type is ${\mu }^{\mathsf{M}}{F}_{\mathsf{T}}\to \mathbf{1}$. The two domains are $R$ and ${\mu }^{\mathsf{M}}{F}_{\mathsf{T}}$, and the universal $R$ cannot be converted to the fixed point. The self-application program therefore fails at the exact place where it would export the negative embedded function.

Proof of Lemma 84.4 — Abstract-domain confinement

Proof. Relate an arbitrary $R$ to a one-point copy $R^{\prime }$ by a relation that contains exactly the $R$-components selected from $u$. Parametricity of $\varphi :\prod _{R:{\mathcal{U}}_i}(R\to A)\to F(R)\to A$ requires its result to be invariant under this relation. A call $\mathit{rec}(r)$ is related only when $r$ belongs to the selected $R$-components. A value constructed at the fixed point has no related $R^{\prime }$ witness, because $R$ is abstract. Hence such a call would violate the relational interpretation of the universal quantifier. ◻

The lemma depends on the parametric model of the universal quantifier. It is not a syntactic theorem about every host language with a rank-polymorphic type. Abel, Matthes, and Uustalu embed their precise Mendler systems in a strongly normalizing $F^{\omega }$ calculus and obtain strong normalization at that signature [AMU05].

Proof of Theorem 84.5 — Mendler iteration normalization, imported

Imported proof. The theorem covers that calculus. It does not cover arbitrary primitive recursion, destructors, histomorphisms, dependent eliminators, or host-language effects. The translation and normalization proof are on pp. 27–35 of [AMU05]. ◻

Nested parameters require a generalized fold

A lambda binder changes the type of variables in its body. Let $$\mathsf{Incr}(A):=\mathbf{1}+A$$ with constructors $\mathsf{zeroV}:=\mathsf{inl}(\star )$ and $\mathsf{sucV}(a):=\mathsf{inr}(a)$. Define the nested family The recursive occurrence in the lambda constructor is at a different parameter. Thus $\mathsf{Term}$ is a nested datatype: its family members are defined together, and one constructor moves from $A$ to $\mathsf{Incr}(A)$.

An ordinary fold to one fixed result type loses the changing parameter. The result must itself be a family $N:{\mathcal{U}}_i\to {\mathcal{U}}_i$, and every method must be polymorphic in the variable type.

The map $k$ reconciles the two ways to extend the variable parameter: $\mathsf{Incr}(M(A))$ and $M(\mathsf{Incr}(A))$. Without it, the lambda clause is ill typed. Bird and Paterson derive this generalized fold and its naturality/fusion laws at the same nested representation [BP99].

For ordinary renaming, take $M$ and $N$ to be the identity family. Define and define The lambda equation is the first nonuniform recursive call: its function has changed from $f:A\to B$ to $\mathsf{lift}(f):\mathsf{Incr}(A)\to \mathsf{Incr}(B)$.

Proof of Proposition 84.7 — Renaming fusion

Proof. Use nested induction, strengthening the claim to every variable type $A$. The variable case is beta equality. The application case follows by the two induction hypotheses and congruence for $\mathsf{app}$. In the lambda case, the induction hypothesis at $\mathsf{Incr}(A)$ gives $$\mathsf{rename}(\mathsf{lift}(g),\mathsf{rename}(\mathsf{lift}(f),b))=\mathsf{rename}(\mathsf{lift}(g)\circ \mathsf{lift}(f),b).$$ Case analysis on $\mathsf{zeroV}$ and $\mathsf{sucV}(a)$ proves $$\mathsf{lift}(g)\circ \mathsf{lift}(f)=\mathsf{lift}(g\circ f)$$ pointwise. Congruence for $\mathsf{rename}(-,b)$ and then $\mathsf{lam}$ closes the case. ◻

Capture-free substitution

A substitution $\sigma :A\to \mathsf{Term}(B)$ must be lifted under a binder. The bound variable remains bound; an old free variable is renamed past the new binder.

For the open term $$t:=\mathsf{lam}(\mathsf{app}(\mathsf{var}(\mathsf{zeroV}),\mathsf{var}(\mathsf{sucV}(x)))),$$ substituting $x\mapsto \mathsf{var}(y)$ gives $$\mathsf{lam}(\mathsf{app}(\mathsf{var}(\mathsf{zeroV}),\mathsf{var}(\mathsf{sucV}(y)))).$$ The old bound occurrence remains $\mathsf{zeroV}$; the free replacement is renamed by $\mathsf{sucV}$. This is the observable capture-avoidance step.

Proof of Lemma 84.10 — Rename after lifted substitution

Proof. If $z\equiv \mathsf{zeroV}$, both sides compute to $\mathsf{var}(\mathsf{zeroV})$. If $z\equiv \mathsf{sucV}(a)$, the left side is $$\mathsf{rename}(\mathsf{lift}(g),\mathsf{rename}(\mathsf{sucV},\sigma (a))).$$ By proposition 84.7, this equals renaming by $\mathsf{lift}(g)\circ \mathsf{sucV}$. On each $b:B$, $$\mathsf{lift}(g)(\mathsf{sucV}(b))\equiv \mathsf{sucV}(g(b)).$$ Applying renaming congruence gives the right side. ◻

Proof of Proposition 84.11 — Renaming–substitution fusion

Proof. Use nested induction generalized over $A$. The variable case is reflexivity. The application case uses the two induction hypotheses under $\mathsf{app}$. In the lambda case, unfold both sides. The induction hypothesis at $\mathsf{Incr}(A)$ reduces the goal to pointwise equality of the two lifted substitutions, which is lemma 84.10. Congruence for $\mathsf{lam}$ closes the case. ◻

A dependent Mendler step

Iteration returns a fixed type $A$. A proof about the input requires a result family. At a positive $F$ with an action, the dependent step must be told how an abstract recursive carrier embeds into the fixed point; only then can it state the indices of its induction hypotheses.

The embedding $e$ records the fixed-point value denoted by each abstract component. Without $e$, the motive $P$ cannot be stated at an abstract recursive argument.

Proof of Proposition 84.13 — Dependent Mendler induction

Proof. Use ordinary fixed-point induction with motive $P$. At a layer $u:F({\mu }^{\mathsf{M}}F)$, the induction hypotheses have type $P(r)$ at every recursive component $r$. Instantiate $\psi$ with $R:={\mu }^{\mathsf{M}}F$ and $e:=\mathsf{id}$. Then ${\mathsf{map}}_F(e,u)=u$ by the identity action law, so the result has type $P({\mathsf{in}}_F^{\mathsf{M}}(u))$. The ordinary computation equation gives the displayed equality. ◻

The construction proves no induction principle for a negative $F$, because its proof uses ${\mathsf{map}}_F$ and the ordinary positive fixed-point induction principle. Dependent Mendler encodings that recover induction use additional identity-mapping or cast structure; their exact support is a separate signature, not an automatic consequence of definition 84.2.

Mixed variance and the hierarchy boundary

The operator $$F_{\mathsf{Foo}}(R):=\mathbf{1}+((R\to R)\times R)$$ has both a negative and a positive occurrence of $R$. It has no ordinary covariant action. A Mendler algebra can nevertheless consume one layer: The embedded function $f:R\to R$ may transform the child $r:R$, and the recursive call may consume the result. It cannot receive a larger fixed-point value containing $f$, because its domain is the abstract type $R$.

This example marks the exact strength of the catamorphism. A Mendler histomorphism additionally exposes an unrolling function for recursive components. At the same negative operator, that extra observation permits an embedded function to be applied to a value that contains the function itself. Ahn and Sheard give the concrete $\mathsf{Foo}$ value and $\mathsf{loopFoo}$ reduction in their Figure 13 [AS11].

Proof of Theorem 84.14 — Hierarchy boundary, imported

Imported proof. Consequently “Mendler style” is not a termination theorem for the entire hierarchy. Iterator, primitive-recursive, destructor, course-of-value, and histomorphism interfaces must be checked separately. The terminating catamorphism instance and the divergent histomorphism trace are the rank-zero results surrounding Figure 13 on printed p. 242 of [AS11]. ◻

The type-constraint boundary

The abstraction argument above controls one recursion scheme. Mendler’s earlier second-order calculus gives a different theorem: strong normalization for an equational recursive-type constraint set satisfying a syntactic positivity condition.

The positive constraint $$\tau =A\to \tau$$ passes the direct polarity check: the recursive atom occurs in the codomain. Change only the direction of the final arrow: $$\tau =\tau \to A.$$ Now $\tau$ occurs negatively in a type equal to itself, so property $P$ fails. The failure has an operational witness. Put $$\delta :=\lambda x:\tau .xx.$$ Conversion by $\tau =\tau \to A$ gives both $x:\tau \to A$ and $\delta :\tau$, hence $$\delta \delta ⟶\delta \delta .$$ This is an explicit reducing cycle, so the changed calculus is divergent; we are not merely observing that a theorem no longer applies.

Proof of Theorem 84.16 — Constraint normalization, imported

Imported proof. The reducibility proof orders only the finitely many constraint classes that occur in a typing derivation, splits each class into positive and negative components, and interprets arrow domains contravariantly. Proposition 10 states the partition criterion, and the following subsection performs the strong-normalization construction [Men91]. The theorem does not range over dependent types, arbitrary type-level computation, or the later Mendler-combinator hierarchy. ◻

Bibliographic note

The rank-polymorphic iteration and generalized higher-kinded schemes follow Abel, Matthes, and Uustalu [AMU05]. The nested de Bruijn representation, generalized fold, and fusion route follow Bird and Paterson [BP99]. The negative-datatype and histomorphism boundary follows Ahn and Sheard [AS11]. Property $P$ and its reducibility boundary are reconstructed from Mendler’s original constraint calculus [Men91].

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 84.7, exercise 84.10.

Exercise 84.7¶

★★☆ Define Mendler algebras for list sum and list append. Expand their equations at nil and cons. For append, state which list is represented by the result type and why no destructor for the first list is required.

Referenced from 4 locations

• Mendler Recursion, Nested Datatypes, and Mixed Variance
• ch:mendler-recursion: ch:mendler-recursion

Exercise 84.8¶

★★★ Prove substitution composition for the nested terms: $$\mathsf{subst}(\tau ,\mathsf{subst}(\sigma ,t))=\mathsf{subst}(\lambda a.\mathsf{subst}(\tau ,\sigma (a)),t).$$ Strengthen the induction over the variable type and prove the lifted- substitution equation needed by the lambda case before using it.

Referenced from 3 locations

• Mendler Recursion, Nested Datatypes, and Mixed Variance
• ch:mendler-recursion: ch:mendler-recursion

Exercise 84.9¶

★★★ Reconstruct the typing failure of the attempted negative destructor and the typing success of ${\varphi }_{\mathsf{len}}$. Then transcribe the source’s $\mathsf{loopFoo}\mathsf{foo}$ example and display two repeated stages of its reduction. Keep the catamorphism and histomorphism signatures distinct.

Referenced from 3 locations

• Mendler Recursion, Nested Datatypes, and Mixed Variance
• ch:mendler-recursion: ch:mendler-recursion

Exercise 84.10¶

★★★ Practical project.mendler-nested-terms Implement in Kappa the nested variable constructors, lambda terms, lifting, renaming, and capture-free substitution of definition 84.8, definition 84.9. Maintain the invariant that entering a lambda maps the bound variable to zeroV and shifts every substituted free variable exactly once. On the named open term $\lambda .\mathsf{app}(\mathsf{zeroV},\mathsf{sucV}(0))$, substitute the free variable $0$ by free variable $7$ and print $\lambda .\mathsf{app}(\mathsf{zeroV},\mathsf{sucV}(7))$. Check renaming identity and the named two-step fusion instance. Reject a mutation that does not shift the substituted free variable with the witness capture-detected. The acceptance test requires the exact normal form, both laws, the rejection witness, and audit result [].

Referenced from 5 locations

• Mendler Recursion, Nested Datatypes, and Mixed Variance
• Object calculus checker and evaluator
• ch:mendler-recursion: ch:mendler-recursion