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.
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.