haskell - ¿Cuándo es una composición de catamorfismos un catamorfismo?

functional-programming composition (4)

Desde la página 3 de http://research.microsoft.com/en-us/um/people/emeijer/Papers/meijer94more.pdf :

no es verdad en general que los catamorfos son cerrados bajo composición

¿En qué condiciones los catamorfismos componen un catamorfismo? Más específicamente (suponiendo que entendí la declaración correctamente):

Supongamos que tengo dos funtores base F y G y pliegues para cada uno: foldF :: (F a -> a) -> (μF -> a) y foldG :: (G a -> a) -> (μG -> a)

Ahora supongamos que tengo dos álgebras a :: F μG -> μG b :: GX -> X

Cuando es la composición (foldG b) . (foldF a) :: μF -> X (foldG b) . (foldF a) :: μF -> X un catamorfismo?

Editar: tengo una suposición, basada en la respuesta expandida de dblhelix: esa outG . a :: F μG -> G μG outG . a :: F μG -> G μG debe ser el componente en μG de alguna transformación natural η :: F a -> G a . No sé si esto es correcto. ( Editar 2: Como colah señala, esto es suficiente, pero no necesario).

Editar 3: Wren Thornton en Haskell-Cafe agrega: "Si tienes el tipo correcto de propiedad distributiva (como colah sugiere) entonces las cosas funcionarán para el caso particular. Pero tener el tipo correcto de propiedad distributiva normalmente equivale a ser un transformación natural en alguna categoría apropiadamente relacionada, de modo que simplemente se difiere la pregunta de si siempre existe una categoría apropiadamente relacionada, y si podemos formalizar lo que significa "apropiadamente relacionado" significa ".

Los catamorfismos deconstruyen una estructura de datos en un valor de resultado. Entonces, en general, cuando aplicas un catamorfismo, el resultado es algo completamente diferente, y no puedes aplicar otro catamorfismo a él.

Por ejemplo, una función que suma todos los elementos de [Int] es un catamorfismo, pero el resultado es Int . No hay forma de cómo aplicar otro catamorfismo en él.

Sin embargo, algunos catamorfismos especiales crean un resultado del mismo tipo que la entrada. Un ejemplo de esto es el map f (para alguna función dada f ). Mientras deconstruye la estructura original, también crea una nueva lista como resultado. (En realidad, el map f se puede ver como un catamorfismo y como un anamorfismo .) De modo que si tienes una clase de catamorfismos tan especial, puedes componerlos.

Si consideramos la equivalencia semántica, la composición de dos catamorfismos es un catamorfismo, cuando el primero es un hilomorfismo:

cata1 . hylo1 = cata2

Por ejemplo (Haskell):

sum . map (^2) = foldl'' (/x y -> x + y^2) 0

(Descargo de responsabilidad: esto está fuera de mi área de especialización. Creo que estoy en lo correcto (con advertencias proporcionadas en diferentes puntos), pero ... Verifíquelo usted mismo.)

Se puede pensar en un catamorfismo como una función que reemplaza a los constructores de un tipo de datos con otras funciones.

(En este ejemplo, usaré los siguientes tipos de datos:

data [a] = [] | a : [a] data BinTree a = Leaf a | Branch (BinTree a) (BinTree a) data Nat = Zero | Succ Nat

)

Por ejemplo:

length :: [a] -> Nat length = catamorphism [] -> 0 (_:) -> (1+)

(Tristemente, la sintaxis de catamorphism {..} no está disponible en Haskell (vi algo similar en Pola). He querido escribir un cuasiquoter para ello.)

Entonces, ¿qué es la length [1,2,3] ?

length [1,2,3] length (1 : 2 : 3 : []) length (1: 2: 3: []) 1+ (1+ (1+ (0 ))) 3

Dicho esto, por razones que se pondrán de manifiesto más adelante, es mejor definirlo como el equivalente trivial:

length :: [a] -> Nat length = catamorphism [] -> Zero (_:) -> Succ

Consideremos algunos ejemplos más de catamorfismos:

map :: (a -> b) -> [a] -> b map f = catamorphism [] -> [] (a:) -> (f a :) binTreeDepth :: Tree a -> Nat binTreeDepth = catamorphism Leaf _ -> 0 Branch -> /a b -> 1 + max a b binTreeRightDepth :: Tree a -> Nat binTreeRightDepth = catamorphism Leaf _ -> 0 Branch -> /a b -> 1 + b binTreeLeaves :: Tree a -> Nat binTreeLeaves = catamorphism Leaf _ -> 1 Branch -> (+) double :: Nat -> Nat double = catamorphism Succ -> Succ . Succ Zero -> Zero

Muchos de estos pueden ser muy bien compuestos para formar nuevos catamorfismos. Por ejemplo:

double . length . map f = catamorphism [] -> Zero (a:) -> Succ . Succ double . binTreeRightDepth = catamorphism Leaf a -> Zero Branch -> /a b -> Succ (Succ b)

double . binTreeDepth double . binTreeDepth también funciona, pero es casi un milagro, en cierto sentido.

double . binTreeDepth = catamorphism Leaf a -> Zero Branch -> /a b -> Succ (Succ (max a b))

Esto solo funciona porque el double distribuye sobre el max ... Lo cual es pura coincidencia. (Lo mismo es cierto con double . binTreeLeaves .) Si reemplazamos max con algo que no funcionó tan bien con el doblamiento ... Bueno, defínanos un nuevo amigo (que no se lleva bien con los demás) . Para los operadores binarios que el double no se distribuye, usaremos (*) .

binTreeProdSize :: Tree a -> Nat binTreeProdSize = catamorphism Leaf _ -> 0 Branch -> /a b -> 1 + a*b

Tratemos de establecer condiciones suficientes para dos catamorfismos que dos componen. Claramente, cualquier catamorfismo se compondrá felizmente con length , double y map f porque ceden su estructura de datos sin mirar los resultados del niño. Por ejemplo, en el caso de la length , puedes reemplazar a Succ y Zero con lo que quieras y tienes tu nuevo catamorfismo.

Si el primer catamorfismo produce una estructura de datos sin mirar lo que le sucede a sus hijos, dos catamorfismos se transformarán en un catamorfismo.

Más allá de esto, las cosas se vuelven más complicadas. Vamos a diferenciar entre los argumentos de constructor normales y los "argumentos recursivos" (que marcaremos con un signo%). Entonces Leaf a no tiene argumentos recursivos, pero Branch %a %b hace. Usemos el término "fijación recursiva" de un constructor para referirnos al número de argumentos recursivos que tiene. (¡He inventado ambos términos! ¡No tengo idea de cuál es la terminología correcta, si es que hay alguno! ¡Tenga cuidado de usarlos en otro lugar!)

Si el primer catamorfismo mapea algo en un constructor de fijación recursivo cero, ¡todo está bien!

a | b | cata(b.a) ===============================|=========================|================ F a %b %c .. -> Z | Z -> G a b .. | True

Si asignamos niños directamente a un nuevo constructor, también somos buenos.

a | b | cata(b.a) ===============================|=========================|================= F a %b %c .. -> H %c %d .. | H %a %b -> G a b .. | True

Si mapeamos en un fixing recursivo un constructor ...

Pero no es iff. Por ejemplo, si existe g1 g2 tal que g (fa b..) = f (g1 a) (g2 b) .. , eso también funciona.

Desde aquí, las reglas se volverán más desordenadas, espero.

When is the composition (fold2 g) . (fold1 f) :: μF1 -> A a catamorphism?

Cuando existe un F1 -algebra h :: F1 A -> A tal que fold1 h = fold2 g . fold1 f fold1 h = fold2 g . fold1 f .

Para ver que los catamorfismos en general no están cerrados en la composición, considere las siguientes definiciones genéricas de punto fijo de nivel de tipo, álgebra y catamorfismo:

newtype Fix f = In {out :: f (Fix f)} type Algebra f a = f a -> a cata :: Functor f => Algebra f a -> Fix f -> a cata phi = phi . fmap (cata phi) . out

Para que los catamorfos compongan, necesitaríamos

algcomp :: Algebra f (Fix g) -> Algebra g a -> Algebra f a

Ahora intenta escribir esta función. Toma dos funciones como argumentos (de tipos f (Fix g) -> Fix g y ga -> a respectivamente) y un valor de tipo fa , y necesita producir un valor de tipo a . ¿Cómo lo harías tú? Para producir un valor de tipo a su única esperanza es aplicar la función de tipo ga -> a , pero luego estamos estancados: no tenemos medios para convertir un valor de tipo fa en un valor de tipo ga , ¿o sí?

No estoy seguro de si esto es útil para sus propósitos, pero un ejemplo de una condición bajo la cual uno puede componer catamorfismos es si tenemos un morfismo desde el resultado de la segunda cata hasta el punto fijo del segundo functor:

algcomp'' :: (Functor f, Functor g) => (a -> Fix g) -> Algebra f (Fix g) -> Algebra g a -> Algebra f a algcomp'' h phi phi'' = cata phi'' . phi . fmap h