General

Creo que veo bien por dónde viene la mano.
Al menos pensando en analogía con las propiedades del producto y coproducto porque son más sencillas y todavía no entiendo bien el caso general de anamorfismos y catamorfismos, jeje.

El chiste es que para el coproducto (un catamorfismo con la propiedad universal)

A -> A+B <- B

   \ f    | F   /g

          C

vamos a tener F . i_A = f. (Con i_X las coproyecciones.)

Para que quede claro, el A+B es de la forma {i_A(a_1),  i_A(a_2), ..., i_B(b_1), ...}. Si hacemos F(A+B) obtenemos {f(a_1), f(a_2), ..., g(b_1), ...} y da la sensación que el catamorfismo lo que hace es transformar i_A en f e i_B en g. Análogo a cómo el foldr transforma el cons y el nil.

Pero usamos fuertemente que el F está a la izquierda del i_A e i_B en el diagrama.

En cambio el producto es un anamorfismo con la propiedad universal y el F está a la derecha, por ende no se puede hacer el mismo truco de "transformar" los constructores.

En resumen no se va a poder hacer con listas tampoco, o esa es mi intuición.

Perdón si quedó demasiado técnica la pregunta, jaja. Me parecía re útil si se podía pensar el unfoldr como transformación de constructores pero creo que no se puede.

Saludos!

Hola,

Respondo medio rápido tus preguntas. Capaz podemos hablarlo mejor al final de la clase.

> Existe una manera similar de razonar el unfoldr en vez de como máquinas de estado?

El recurso de máquina de estado se usa en general como forma intuitiva de entender al unfoldr como la función que retorna el comportamiento observacional de una máquina. En el caso de unfoldr ese comportamiento es dado por una lista, pero se puede generalizar para otras estructuras. Del lado de la programación lo podemos ver como un mecanismo de estructuración de código como ocurre con foldr.

Capaz que el tipo confunde porque unfoldr mapea una coálgebra cualquiera en la "coálgebra final" que viene dada por el destructor destr : [a] -> 1 + (a,[b]) que en Haskell se escribe [a] -> Maybe (a,[a]). Lo que ocurre es que, visto como función, el destructor es la inversa de los constructores. En efecto, hay un isomorfismo entre [a] y 1 + (a,[a]). La inversa es la función constr : 1 + (a,[a]) -> [a]. Hay además un tema un poco técnico; lo que anoto como [a] en realidad debería anotarlo de otra forma porque no corresponde al tipo inductivo de las listas, sino al coinductivo. Depende de cual sea el dominio de interpretación de los tipos y las funciones. Si el dominio es Set entonces el tipo inductivo corresponde a las listas finitas y el coinductivo al tipo de las listas finitas + las infinitas.

Una introducción muy buena al tema desde una perspectiva algebraica/coalgebraica es el siguiente tutorial de Bart Jacobs y Jan Rutten: A tutorial on (co)algebras and (co)induction, Bulletin-European Association for Theoretical Computer Science, vol. 62, 1997. Está online.

Saludos,
Alberto.