patternMinor
Functorial type constructors in System F
Viewed 0 times
typeconstructorssystemfunctorial
Problem
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.
Can someone explain why this is true or refer me to a proof? Because I have not found a proof for this claim yet.
Solution
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}$$
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}$$
Context
StackExchange Computer Science Q#72384, answer score: 7
Revisions (0)
No revisions yet.