I'm studying how coinduction was encoded in Isabelle. At page 7 of the attached document, the author describes how some datatypes can be encoded as initial algebras. Here is one example:

Finite lists

The unary type constructor list, which sends each type α to the type α list of lists of α elements, is categorically given as the initial algebra on the second argument of the binary functor (F, Fmap), where (α, β) F = unit+α×β and Fmap f g = id⊕ f ⊗g.

More precisely, there exists a (polymorphic) folding bijection fld : (α, α list) F → α list making (fld, α list) the initial algebra for the unary functor (α, _) F. Here, fld = $\langle$Nil, Cons$\rangle$, where Nil and Cons are the familiar list operations. The initial algebra property corresponds to the availability of the standard iterator for lists. Then (list, map) is itself a unary functor.

First parragraph

If $U$ is the set of types. $F: U \times U \to U$ is a functor which on objects acts like $F(\alpha,\beta) = unit+\alpha \times \beta$ and on morphisms acts as $F((f,g)) = id \oplus f \otimes g$. As usual, this functor will lead to another functor if we fix $\alpha$. Let's call it $G$. Then, one defines lists as being the initial algebra (if it exists) for the functor $G$. Let's call $\alpha \; list$ the carrier of that algebra.

I think initial algebras for polynomial functors $F: Set \to Set$ always exist so let's drop the existence matter here.

Second parragraph

$fld$ seems to be the structure mapping of the coalgebra $fld: G(\alpha \; list) \to \alpha \; list$. So in my notation the $G$-algebra is $(\alpha \; list, fld)$. One may check that $\langle Nil, Cons \rangle$ make $fld$ work in the initiality diagram.


What is meant by the standard "iterator" for lists?

Where was $(list,map)$ defined? (I think nowhere). What is the author transmitting by saying that $(list,map)$ is a unary functor?

It may be worth reading the following section on "Finitely branching trees of finite depth" in the linked thesis.

  • $\begingroup$ The standard iterator on lists is the catamorphism, which corresponds to the foldr operation (for some specific element type). $\endgroup$
    – Labbekak
    Apr 1, 2020 at 7:02


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.