5
$\begingroup$

I have come across the claim that all basic data types in System F, such as Bool, Nat, and List(U), can be expressed in the form $\forall \alpha (((T\alpha \rightarrow \alpha) \rightarrow \alpha)$, where $T(\alpha)$ is a definable functorial type constructor.

Can someone explain why this is true or refer me to a proof? Because I have not found a proof for this claim yet.

$\endgroup$
7
$\begingroup$

The usual (categorical) characterization of inductive data types is as initial $F$-algebras for a functor $F$. An $F$-algebra is a pair of a type, $A$, and a function $a : FA \to A$. A homomorphism of $F$-algebras, $\varphi : (A,a) \to (B,b)$ is a function $\varphi : A \to B$ which satisfies $\varphi\circ a = b\circ F\varphi$. An $F$-algebra, $(\mu F,\mathsf{in}_F)$, is initial if there exists a unique homomorphism from it to any other $F$-algebra. This means we have a function which takes an $F$-algebra $(A,a)$ and produces a function $\mathsf{fold}_A(a):\mu F\to A$ which satisfies $$\mathsf{fold}_A(a)\circ\mathsf{in}_F=a\circ F(\mathsf{fold}_A(a))$$ The type of $\mathsf{fold}$ in System F would be $\forall \alpha.(F\alpha\to\alpha)\to\mu F\to\alpha$. The free theorem for this (as calculated by this) specializes to $$\forall \alpha,\beta. \forall \varphi : \alpha\to \beta. \forall a : F \alpha \to \alpha. \forall b : F \beta \to \beta.\\ \varphi \circ a = b \circ F \varphi \implies \varphi \circ \mathsf{fold}_{\alpha}(a) = \mathsf{fold}_\beta(b)$$ which further specializes to $$\forall \beta. \forall b : F \beta \to \beta. b\circ \mathsf{fold}_{F\beta}(Fb) = \mathsf{fold}_\beta(b)$$ and $$\forall \beta. \forall \varphi : \mu F\to \beta. \forall b : F \beta \to \beta.\\ \varphi \circ \mathsf{in}_F = b \circ F \varphi \implies \varphi \circ \mathsf{fold}_{\mu F}(\mathsf{in}_F) = \mathsf{fold}_\beta(b)$$ If we can prove $\mathsf{fold}_{\mu F}(\mathsf{in}_F) = id_{\mu F}$, then this would mean that $(\mu F,\mathsf{in}_F)$ was an initial $F$-algebra as the above equation says: "any $F$-algebra homomorphism $\varphi : (\mu F, \mathsf{in}_F)\to(B,\beta)$ is $\mathsf{fold}_\beta(b)$ and thus exists and is unique". Of course to do this we need to actually give a definition of $\mu F$, $\mathsf{fold}$, and $\mathsf{in}_F$.

By noting that $\forall \alpha.(F\alpha\to\alpha)\to\mu F\to\alpha$ is isomorphic to $\mu F \to \forall \alpha.(F\alpha\to\alpha)\to\alpha$, there's an obvious choice for both $\mathsf{fold}$ and $\mu F$: simply set $\mu F = \forall \alpha.(F\alpha\to\alpha)\to\alpha$ and $\mathsf{fold}$ to be the inverse image of $id$ with respect to that isomorphism. Explicitly, $$\mathsf{fold} = \Lambda\alpha.\lambda a\!:\!F\alpha\to\alpha.\lambda g\!:\!\mu F.g[\alpha]a$$ All that remains is to define $\mathsf{in}_F$ and show that $\mathsf{fold}_{\mu F}(\mathsf{in}_F) = id_{\mu F}$. The easiest way to define $\mathsf{in}_F$ is to just follow the types: $\mathsf{in}_F : F\mu F \to \forall \alpha.(F\alpha\to\alpha) \to \alpha$ so $$\mathsf{in}_F = \lambda x\!:\!F\mu F.\Lambda\alpha.\lambda a\!:\!F\alpha\to\alpha.a(F(\mathsf{fold}_{\alpha}(a))x)$$ This definition is particularly convenient as you may have noticed that while I've shown that if there's a homomorphism $\varphi : (\mu F,\mathsf{in}_F)\to(A,a)$ then it is $\mathsf{fold}_A(a)$, and I've shown that there is a function $\mathsf{fold}_A(a):\mu F\to A$, I haven't shown that $\mathsf{fold}_A(a)$ is a homomorphism. That is, I haven't shown $\mathsf{fold}_A(a)\circ\mathsf{in}_F = a\circ F(\mathsf{fold}_A(a))$, but with the above definitions of $\mathsf{fold}$ and $\mathsf{in}_F$ this is easily shown by normalizing. To finish, $$\begin{align} \mathsf{fold}_{\mu F}(\mathsf{in}_F) & = \mathsf{in}_F\circ\mathsf{fold}_{F\mu F}(F(\mathsf{in}_F)) \\ & = \lambda g\!:\!\mu F.\Lambda\alpha.\lambda a\!:\!F\alpha\to\alpha.(a\circ F(\mathsf{fold}_{\alpha}(a)) \circ \mathsf{fold}_{F\mu F}(F(\mathsf{in}_F)))g \\ & = \lambda g\!:\!\mu F.\Lambda\alpha.\lambda a\!:\!F\alpha\to\alpha.(\mathsf{fold}_\alpha(a)\circ \mathsf{in}_F \circ \mathsf{fold}_{F\mu F}(F(\mathsf{in}_F)))g \\ & = \lambda g\!:\!\mu F.\Lambda\alpha.\lambda a\!:\!F\alpha\to\alpha.(\mathsf{fold}_\alpha(a)\circ \mathsf{fold}_{\mu F}(\mathsf{in}_F))g \\ & = \lambda g\!:\!\mu F.\Lambda\alpha.\lambda a\!:\!F\alpha\to\alpha.\mathsf{fold}_\alpha(a)g \\ & = \lambda g\!:\!\mu F.\Lambda\alpha.\lambda a\!:\!F\alpha\to\alpha.g[\alpha]a \\ & = \lambda g\!:\!\mu F.g \end{align}$$

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.