Catamorfismo

En programación funcional , el concepto de catamorfismo (del griego antiguo : κατά "hacia abajo" y μορφή "forma, figura") denota el homomorfismo único de un álgebra inicial en alguna otra álgebra.

Los catamorfismos proporcionan generalizaciones de los pliegues de listas a tipos de datos algebraicos arbitrarios , que pueden describirse como álgebras iniciales . El concepto dual es el de anamorfismo que generaliza los desdoblamientos . Un hilemorfismo es la composición de un anamorfismo seguido de un catamorfismo.

Definición

Considérese una -álgebra inicial para algún endofunctor de alguna categoría en sí mismo. Aquí hay un morfismo de a . Puesto que es inicial, sabemos que siempre que es otra -álgebra, es decir, un morfismo de a , hay un homomorfismo único de a . Por la definición de la categoría de -álgebra, esto corresponde a un morfismo de a , convencionalmente también denotado , tal que . En el contexto de -álgebra, el morfismo especificado de forma única del objeto inicial se denota por y, por tanto, se caracteriza por la siguiente relación: ${\displaystyle F}$ ${\displaystyle (A,in)}$ ${\displaystyle F}$ ${\displaystyle in}$ ${\displaystyle FA}$ ${\displaystyle A}$ ${\displaystyle (X,f)}$ ${\displaystyle F}$ ${\displaystyle f}$ ${\displaystyle FX}$ ${\displaystyle X}$ ${\displaystyle h}$ ${\displaystyle (A,in)}$ ${\displaystyle (X,f)}$ ${\displaystyle F}$ ${\displaystyle h}$ ${\displaystyle A}$ ${\displaystyle X}$ ${\displaystyle h}$ ${\displaystyle h\circ in=f\circ Fh}$ ${\displaystyle F}$ ${\displaystyle \mathrm {cata} \ f}$

• ${\displaystyle h=\mathrm {cata} \ f}$
• ${\displaystyle h\circ in=f\circ Fh}$

Terminología e historia

Otra notación que se encuentra en la literatura es . Los corchetes abiertos utilizados se conocen como corchetes banana , después de lo cual los catamorfismos a veces se denominan bananas , como se menciona en Erik Meijer et al . ^[1] Una de las primeras publicaciones en introducir la noción de catamorfismo en el contexto de la programación fue el artículo “Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire”, de Erik Meijer et al. , ^[1] que estaba en el contexto del formalismo Squiggol . La definición categórica general fue dada por Grant Malcolm. ^{[2] [3]} ${\displaystyle (\!|f|\!)}$

Ejemplos

Damos una serie de ejemplos, y luego un enfoque más global de los catamorfismos, en el lenguaje de programación Haskell .

Catamorfismo para el álgebra de los tal vez

Considere el functor Maybedefinido en el siguiente código Haskell:

datos Tal vez un = Nada | Solo un -- Tal vez tipo        clase Functor f donde -- clase para funtores fmap :: ( a -> b ) -> ( f a -> f b ) -- acción del functor sobre morfismos                instancia Functor Maybe donde -- convierte Maybe en un functor fmap g Nothing = Nothing fmap g ( Just x ) = Just ( g x )                 

El objeto inicial del Álgebra-Tal vez es el conjunto de todos los objetos de tipo número natural Natjunto con el morfismo inidefinido a continuación: ^{[4] [5]}

datos Nat = Zero | Succ Nat -- tipo de número natural       ini :: Maybe Nat -> Nat -- objeto inicial del álgebra Maybe (con un ligero abuso de notación) ini Nada = Cero ini ( Solo n ) = Succ n              

El catamapa se puede definir de la siguiente manera: ^[5]

cata :: ( Maybe b -> b ) -> ( Nat -> b ) cata g Cero = g ( fmap ( cata g ) Nada ) -- Nota: fmap (cata g) Nada = g Nada y Cero = ini(Nada) cata g ( Succ n ) = g ( fmap ( cata g ) ( Solo n )) -- Nota: fmap (cata g) (Solo n) = Solo (cata gn) y Succ n = ini(Solo n)                            

Como ejemplo consideremos el siguiente morfismo:

g :: Quizás String -> String g Nada = "¡vete!" g ( Solo str ) = "espera..." ++ str               

Entonces cata g ((Succ. Succ . Succ) Zero)evaluará "espera... espera... espera... ¡vete!".

Lista plegable

Para un tipo fijo aconsidere el functor MaybeProd adefinido por lo siguiente:

datos MaybeProd a b = Nothing | Just ( a , b ) -- (a,b) es el tipo de producto de a y b          clase Functor f donde -- clase para funtores fmap :: ( a -> b ) -> ( f a -> f b ) -- acción del functor sobre morfismos                instancia Functor ( MaybeProd a ) donde -- convierte MaybeProd a en un functor, la funtorialidad está solo en la segunda variable de tipo fmap g Nothing = Nothing fmap g ( Just ( x , y )) = Just ( x , g y )                   

El álgebra inicial de MaybeProd aestá dada por las listas de elementos con tipo ajunto con el morfismo inidefinido a continuación: ^[6]

datos Lista a = ListaVacía | Cons a ( Lista a )         ini :: MaybeProd a ( Lista a ) -> Lista a -- álgebra inicial de MaybeProd a ini Nothing = EmptyList ini ( Just ( n , l )) = Cons n l                  

El catamapa se puede definir por:

cata :: ( MaybeProd a b -> b ) -> ( List a -> b ) cata g EmptyList = g ( fmap ( cata g ) Nothing ) -- Nota: ini Nothing = EmptyList cata g ( Cons s l ) = g ( fmap ( cata g ) ( Just ( s , l ))) -- Nota: Cons sl = ini (Just (s,l))                               

Observe también que cata g (Cons s l) = g (Just (s, cata g l)). Como ejemplo, considere el siguiente morfismo:

g :: MaybeProd Int Int -> Int g Nada = 3 g ( Sólo ( x , y )) = x * y             

cata g (Cons 10 EmptyList)evalúa a 30. Esto se puede ver expandiendo cata g (Cons 10 EmptyList)=g (Just (10,cata g EmptyList)) = 10* cata g EmptyList=10* g Nothing=10*3.

De la misma manera se puede demostrar que esto cata g (Cons 10 (Cons 100 (Cons 1000 EmptyList)))se evaluará como 10*(100*(1000*3))=3.000.000.

El catamapa está estrechamente relacionado con el pliegue derecho (ver Pliegue (función de orden superior) ) de listas foldrList. El morfismo liftdefinido por

ascensor :: ( a -> b -> b ) -> b -> ( MaybeProd a b -> b ) ascensor g b0 Nada = b0 ascensor g b0 ( Sólo ( x , y )) = g x y                           

se relaciona catacon el pliegue derecho foldrListde las listas a través de:

foldrList :: ( a -> b -> b ) -> b -> Lista a -> b foldrList fun b0 = cata ( lift fun b0 )                   

La definición de cataimplica que foldrListes el pliegue derecho y no el pliegue izquierdo. Por ejemplo: foldrList (+) 1 (Cons 10 ( Cons 100 ( Cons 1000 EmptyList)))se evaluará como 1111 y foldrList (*) 3 (Cons 10 ( Cons 100 ( Cons 1000 EmptyList)))como 3.000.000.

Pliegue del árbol

Para un tipo fijo a, considere el functor que asigna tipos ba un tipo que contiene una copia de cada término de aasí como todos los pares de b's (términos del tipo producto de dos instancias del tipo b). Un álgebra consiste en una función a b, que actúa sobre un atérmino o dos btérminos. Esta fusión de un par se puede codificar como dos funciones de tipo a -> brespectivamente b -> b -> b.

tipo TreeAlgebra a b = ( a -> b , b -> b -> b ) -- la función "dos casos" se codifica como (f, g) datos Tree a = Leaf a | Branch ( Tree a ) ( Tree a ) -- que resulta ser el álgebra inicial foldTree :: TreeAlgebra a b -> ( Tree a -> b ) -- los catamorfismos se asignan de (Tree a) a b foldTree ( f , g ) ( Leaf x ) = f x foldTree ( f , g ) ( Branch left right ) = g ( foldTree ( f , g ) left ) ( foldTree ( f , g ) right )                                                           

treeDepth :: TreeAlgebra a Integer -- un f-álgebra para números, que funciona para cualquier tipo de entrada treeDepth = ( const 1 , \ i j -> 1 + max i j ) treeSum :: ( Num a ) => TreeAlgebra a a -- un f-álgebra, que funciona para cualquier tipo de número treeSum = ( id , ( + ))                            

Caso general

Estudios teóricos de categorías más profundos de álgebras iniciales revelan que el F-álgebra obtenida al aplicar el funtor a su propia álgebra inicial es isomorfa a ella.

Los sistemas de tipos fuertes nos permiten especificar de manera abstracta el álgebra inicial de un funtor fcomo su punto fijo a = fa . Los catamorfismos definidos recursivamente ahora se pueden codificar en una sola línea, donde el análisis de caso (como en los diferentes ejemplos anteriores) está encapsulado por el fmap. Dado que el dominio de este último son objetos en la imagen de f, la evaluación de los catamorfismos salta de ida y vuelta entre ay f a.

Álgebra de tipo f a = f a -> a -- las f-álgebras genéricas         newtype Fix f = Iso { invIso :: f ( Fix f ) } - nos da el álgebra inicial para el funtor f            cata :: Functor f => Algebra f a - > ( Fix f -> a ) -- catamorfismo de Fix f a a cata alg = alg.fmap ( cata alg ) .invIso -- note que invIso y alg se asignan en direcciones opuestas                       

Ahora volvemos al primer ejemplo, pero ahora pasando el funtor Maybe a Fix. La aplicación repetida del funtor Maybe genera una cadena de tipos, que, sin embargo, se pueden unir por el isomorfismo del teorema del punto fijo. Introducimos el término zero, que surge de Maybe Nothinge identificamos una función sucesora con la aplicación repetida de Just. De esta manera surgen los números naturales.

tipo Nat = Fix Maybe zero :: Nat zero = Iso Nothing -- cada 'Maybe a' tiene un término Nothing, e Iso lo asigna a un sucesor :: Nat -> Nat successor = Iso . Just -- Simplemente asigna a a 'Maybe a' e Iso lo asigna de nuevo a un nuevo término                   

pleaseWait :: Algebra Maybe String - nuevamente el tonto ejemplo de f-álgebra de arriba pleaseWait ( Just string ) = "espera.. " ++ string pleaseWait Nothing = "¡vete!"              

Nuevamente, lo siguiente se evaluará como "espera... espera... espera... espera... ¡ya!":cata pleaseWait (successor.successor.successor.successor $ zero)

Y ahora, nuevamente el ejemplo del árbol. Para esto, debemos proporcionar el tipo de datos del contenedor del árbol para que podamos configurarlo fmap(no tuvimos que hacerlo para el Maybefunctor, ya que es parte del preludio estándar).

datos Tcon a b = TconL a | TconR b b instancia Functor ( Tcon a ) donde fmap f ( TconL x ) = TconL x fmap f ( TconR y z ) = TconR ( f y ) ( f z )                                

tipo Árbol a = Fix ( Tcon a ) -- el álgebra inicial fin :: a -> Árbol a fin = Iso . TconL encuentro :: Árbol a -> Árbol a -> Árbol a encuentro l r = Iso $ TconR l r                                 

treeDepth :: Algebra ( Tcon a ) Entero -- nuevamente, el ejemplo de f-álgebra de treeDepth treeDepth ( TconL x ) = 1 treeDepth ( TconR y z ) = 1 + max y z                   

Lo siguiente tendrá un puntaje de 4:cata treeDepth $ meet (end "X") (meet (meet (end "YXX") (end "YXY")) (end "YY"))

Véase también

• Morfismo
• Morfismos de las F-álgebras
  • De una coalgebra a una coalgebra final: Anamorfismo
  • Un anamorfismo seguido de un catamorfismo: Hilomorfismo
  • Ampliación de la idea de catamorfismos: Paramorfismo
  • Ampliación de la idea de anamorfismos: Apomorfismo

Referencias

1. Meijer, Erik; Fokkinga, Maarten; Paterson, Ross (1991), Hughes, John (ed.), "Programación funcional con plátanos, lentes, sobres y alambre de púas", Lenguajes de programación funcional y arquitectura informática , vol. 523, Springer Berlin Heidelberg, págs. 124–144, doi :10.1007/3540543961_7, ISBN 978-3-540-54396-1, S2CID  11666139 , consultado el 7 de mayo de 2020
2. Malcolm, Grant Reynold (1990), Tipos de datos algebraicos y transformación de programas (PDF) (tesis doctoral), Universidad de Groningen, archivado desde el original (PDF) el 10 de junio de 2015.
3. Malcolm, Grant (1990), "Estructuras de datos y transformación de programas", Science of Computer Programming , vol. 14, núm. 2-3, págs. 255-279, doi : 10.1016/0167-6423(90)90023-7.
4. "Álgebra inicial de un endofunctor en nLab".
5. "Número natural en nLab".
6. "Álgebra inicial de un endofunctor en nLab".

Lectura adicional

• Ki Yung Ahn; Sheard, Tim (2011). "Una jerarquía de combinadores de recursión de estilo Mendler: domesticando tipos de datos inductivos con ocurrencias negativas". Actas de la 16.ª conferencia internacional ACM SIGPLAN sobre programación funcional . ICFP '11.

Enlaces externos

• Catamorfismos en HaskellWiki
• Catamorfismos de Edward Kmett
• Catamorfismos en fa sostenido (partes 1, 2, 3, 4, 5, 6, 7) por Brian McNamara
• Catamorfismos en Haskell