scala haskell functional-programming programming-languages category-theory

scala - ¿Qué significa “coalgebra” en el contexto de la programación?



haskell functional-programming (4)

He escuchado el término "coalgebras" varias veces en la programación funcional y en los círculos PLT, especialmente cuando la discusión es sobre objetos, comonads, lentes y demás. Buscar en Google en este término proporciona páginas que dan una descripción matemática de estas estructuras, lo cual es bastante incomprensible para mí. ¿Puede alguien explicar por favor qué significan las coalgebras en el contexto de la programación, cuál es su importancia y cómo se relacionan con los objetos y las comonadios?

Álgebras

Creo que el lugar para comenzar sería entender la idea de un álgebra . Esto es solo una generalización de estructuras algebraicas como grupos, anillos, monoides, etc. La mayoría de las veces, estas cosas se presentan en términos de conjuntos, pero como estamos entre amigos, hablaré sobre los tipos de Haskell. (Sin embargo, no puedo resistirme a usar algunas letras griegas, ¡hacen que todo se vea mejor!)

Un álgebra, entonces, es solo un tipo τ con algunas funciones e identidades. Estas funciones toman diferentes números de argumentos del tipo τ y producen un τ : sin prisa, todos se ven como (τ, τ,…, τ) → τ . También pueden tener "identidades": elementos de τ que tienen un comportamiento especial con algunas de las funciones.

El ejemplo más simple de esto es el monoide. Un monoide es cualquier tipo τ con una función mappend ∷ (τ, τ) → τ y una identidad mzero ∷ τ . Otros ejemplos incluyen cosas como grupos (que son como monoides, excepto con una función invert ∷ τ → τ extra), anillos, celosías, etc.

Todas las funciones operan en τ pero pueden tener diferentes aridades. Podemos escribirlos como τⁿ → τ , donde τⁿ asigna a una tupla de n τ . De esta manera, tiene sentido pensar en las identidades como τ⁰ → τ donde τ⁰ es solo la tupla vacía () . Entonces podemos simplificar la idea de un álgebra ahora: es solo un tipo con algunas funciones en él.

Un álgebra es solo un patrón común en matemáticas que se ha "excluido", tal como lo hacemos con el código. Las personas notaron que un montón de cosas interesantes (los monoides mencionados anteriormente, los grupos, las celosías, etc.) siguen un patrón similar, por lo que se abstrajeron. La ventaja de hacer esto es la misma que en la programación: crea pruebas reutilizables y facilita ciertos tipos de razonamiento.

F-Algebras

Sin embargo, no hemos terminado con la factorización. Hasta ahora, tenemos un montón de funciones τⁿ → τ . Podemos hacer un buen truco para combinarlos en una sola función. En particular, veamos los monoides: tenemos mappend ∷ (τ, τ) → τ y mempty ∷ () → τ . Podemos convertirlos en una sola función utilizando un tipo de suma: Either . Se vería así:

op ∷ Monoid τ ⇒ Either (τ, τ) () → τ op (Left (a, b)) = mappend (a, b) op (Right ()) = mempty

Podemos usar esta transformación repetidamente para combinar todas las funciones τⁿ → τ en una sola, para cualquier álgebra. (De hecho, podemos hacer esto para cualquier número de funciones a → τ , b → τ y así sucesivamente para cualquier a, b,… )

Esto nos permite hablar de las álgebras como un tipo τ con una sola función, desde algún desorden de Either de los Either hasta un solo τ . Para los monoides, este lío es: Either (τ, τ) () ; para los grupos (que tienen una operación adicional τ → τ ), es: Either (Either (τ, τ) τ) () . Es un tipo diferente para cada estructura diferente. Entonces, ¿qué tienen en común todos estos tipos? Lo más obvio es que todos son solo sumas de productos: tipos de datos algebraicos. Por ejemplo, para los monoides, podríamos crear un tipo de argumento monoide que funcione para cualquier monoid τ:

data MonoidArgument τ = Mappend τ τ -- here τ τ is the same as (τ, τ) | Mempty -- here we can just leave the () out

Podemos hacer lo mismo para grupos, anillos, celosías y todas las otras estructuras posibles.

¿Qué más hay de especial en todos estos tipos? Bueno, todos son Functors ! P.ej:

instance Functor MonoidArgument where fmap f (Mappend τ τ) = Mappend (f τ) (f τ) fmap f Mempty = Mempty

Así podemos generalizar aún más nuestra idea de un álgebra. Es solo un tipo τ con una función f τ → τ para algún funtor f . De hecho, podríamos escribir esto como una clase de tipos:

class Functor f ⇒ Algebra f τ where op ∷ f τ → τ

Esto a menudo se denomina "álgebra F" porque está determinado por el functor F Si pudiéramos aplicar parcialmente clases de tipos, podríamos definir algo como la class Monoid = Algebra MonoidArgument .

Coalgebras

Ahora, espero que tenga una buena idea de lo que es un álgebra y de cómo se trata de una generalización de las estructuras algebraicas normales. Entonces, ¿qué es una F-coalgebra? Bueno, la compañía implica que es el "dual" de un álgebra, es decir, tomamos un álgebra y tiramos algunas flechas. Solo veo una flecha en la definición anterior, así que solo le daré la vuelta:

class Functor f ⇒ CoAlgebra f τ where coop ∷ τ → f τ

Y eso es todo lo que es! Ahora, esta conclusión puede parecer un poco frívolo (jeje). Le dice qué es una coalgebra, pero en realidad no da ninguna idea de cómo es útil o por qué nos importa. Llegaré a eso en un momento, una vez que encuentre o encuentre un buen ejemplo o dos: P.

Clases y objetos

Después de leer un poco, creo que tengo una buena idea de cómo usar coalgebras para representar clases y objetos. Tenemos un tipo C que contiene todos los estados internos posibles de objetos en la clase; la clase en sí misma es una coalgebra sobre C que especifica los métodos y propiedades de los objetos.

Como se muestra en el ejemplo de álgebra, si tenemos un conjunto de funciones como a → τ b → τ para cualquier a, b,… , podemos combinarlas todas en una sola función utilizando Either , un tipo de suma. La "noción" dual sería combinar un montón de funciones de tipo τ → a , τ → b y así sucesivamente. Podemos hacer esto usando el tipo dual de suma: un tipo de producto. Entonces, dadas las dos funciones anteriores (llamadas f y g ), podemos crear una única como esta:

both ∷ τ → (a, b) both x = (f x, g x)

El tipo (a, a) es un functor de manera directa, por lo que ciertamente encaja con nuestra noción de una F-coalgebra. Este truco en particular nos permite agrupar un montón de funciones diferentes, o, para los métodos OOP, en una sola función de tipo τ → f τ .

Los elementos de nuestro tipo C representan el estado interno del objeto. Si el objeto tiene algunas propiedades legibles, tienen que poder depender del estado. La forma más obvia de hacer esto es hacer de ellos una función de C Entonces, si queremos una propiedad de longitud (por ejemplo, object.length ), tendríamos una función C → Int .

Queremos métodos que puedan tomar un argumento y modificar el estado. Para hacer esto, necesitamos tomar todos los argumentos y producir una nueva C Imaginemos un método setPosition que toma una coordenada x y una y : object.setPosition(1, 2) . Se vería así: C → ((Int, Int) → C) .

El patrón importante aquí es que los "métodos" y "propiedades" del objeto toman el objeto en sí como su primer argumento. Esto es igual que el parámetro self en Python y como el implícito de muchos otros idiomas. Una coalgebra esencialmente simplemente encapsula el comportamiento de tomar un self parámetro: ese es el primer C en C → FC .

Así que vamos a poner todo junto. Imaginemos una clase con una propiedad de position , una propiedad de name y setPosition función setPosition :

class C private x, y : Int _name : String public name : String position : (Int, Int) setPosition : (Int, Int) → C

Necesitamos dos partes para representar esta clase. Primero, necesitamos representar el estado interno del objeto; en este caso solo tiene dos Int s y una String . (Este es nuestro tipo C ). Luego tenemos que crear una coalgebra que represente a la clase.

data C = Obj { x, y ∷ Int , _name ∷ String }

Tenemos dos propiedades para escribir. Son bastante triviales:

position ∷ C → (Int, Int) position self = (x self, y self) name ∷ C → String name self = _name self

Ahora solo necesitamos poder actualizar la posición:

setPosition ∷ C → (Int, Int) → C setPosition self (newX, newY) = self { x = newX, y = newY }

Esto es como una clase de Python con sus self variables explícitas. Ahora que tenemos un montón de funciones self → , necesitamos combinarlas en una sola función para la coalgebra. Podemos hacer esto con una tupla simple:

coop ∷ C → ((Int, Int), String, (Int, Int) → C) coop self = (position self, name self, setPosition self)

El tipo ((Int, Int), String, (Int, Int) → c) —para cualquier c — es un funtor, por lo que coop tiene la forma que queremos: Functor f ⇒ C → f C

Dado esto, C y la coop forman una coalgebra que especifica la clase que di anteriormente. Puede ver cómo podemos usar esta misma técnica para especificar cualquier número de métodos y propiedades para que tengan nuestros objetos.

Esto nos permite usar el razonamiento de coalgebraic para tratar con las clases. Por ejemplo, podemos traer la noción de un "homomorfismo de F-coalgebra" para representar transformaciones entre clases. Este es un término que suena aterrador que simplemente significa una transformación entre coalgebras que preserva la estructura. Esto hace que sea mucho más fácil pensar en la asignación de clases a otras clases.

En resumen, un F-coalgebra representa una clase al tener un montón de propiedades y métodos que dependen de un parámetro que contiene el estado interno de cada objeto.

Otras categorias

Hasta ahora, hemos hablado de álgebras y coalgebras como tipos de Haskell. Un álgebra es solo un tipo τ con una función f τ → τ y una coalgebra es solo un tipo τ con una función τ → f τ .

Sin embargo, nada vincula realmente estas ideas con Haskell en sí . De hecho, generalmente se presentan en términos de conjuntos y funciones matemáticas en lugar de tipos y funciones de Haskell. De hecho, podemos generalizar estos conceptos a cualquier categoría!

Podemos definir un álgebra F para alguna categoría C Primero, necesitamos un funtor F : C → C , es decir, un endofunctor . (Todos los Haskell Functor s son en realidad Hask → Hask de Hask → Hask ). Entonces, un álgebra es solo un objeto A de C con un morfismo FA → A Una coalgebra es la misma excepto con A → FA .

¿Qué ganamos al considerar otras categorías? Bueno, podemos usar las mismas ideas en diferentes contextos. Como las mónadas. En Haskell, una mónada es un tipo M ∷ ★ → ★ con tres operaciones:

map ∷ (α → β) → (M α → M β) return ∷ α → M α join ∷ M (M α) → M α

La función de map es solo una prueba del hecho de que M es un Functor . Entonces podemos decir que una mónada es solo un funtor con dos operaciones: return y join .

Los funcionalizadores forman una categoría por sí mismos, y los morfismos entre ellos se denominan "transformaciones naturales". Una transformación natural es solo una forma de transformar un funtor en otro y preservar su estructura. Here''s un buen artículo que ayuda a explicar la idea. Habla de concat , que es solo join para listas.

Con los functores de Haskell, la composición de dos functores es un functor en sí mismo. En pseudocódigo, podríamos escribir esto:

instance (Functor f, Functor g) ⇒ Functor (f ∘ g) where fmap fun x = fmap (fmap fun) x

Esto nos ayuda a pensar en join como una asignación de f ∘ f → f . El tipo de join es ∀α. f (f α) → f α ∀α. f (f α) → f α . Intuitivamente, podemos ver cómo una función válida para todos los tipos α puede considerarse como una transformación de f .

return es una transformación similar. Su tipo es ∀α. α → f α ∀α. α → f α . ¡Esto se ve diferente, el primer α no está "en" un funtor! Afortunadamente, podemos arreglar esto agregando un functor de identidad allí: ∀α. Identity α → f α ∀α. Identity α → f α . Así que el return es una Identity → f transformación Identity → f .

Ahora podemos pensar en una mónada como solo un álgebra basada en algún función f con operaciones f ∘ f → f e Identity → f . ¿No te parece familiar? Es muy similar a un monoide, que era solo un tipo τ con operaciones τ × τ → τ y () → τ .

Entonces, una mónada es como un monoide, excepto que en lugar de tener un tipo, tenemos un funtor. Es el mismo tipo de álgebra, solo en una categoría diferente. (Aquí es donde la frase "Una mónada es solo un monoide en la categoría de endofunctores" proviene de lo que yo sé.)

Ahora, tenemos estas dos operaciones: f ∘ f → f e Identity → f . Para obtener la coalgebra correspondiente, simplemente tiramos las flechas. Esto nos da dos nuevas operaciones: f → f ∘ f y f → Identity . Podemos convertirlos en tipos Haskell agregando variables de tipo como anteriormente, dándonos ∀α. f α → f (f α) ∀α. f α → f (f α) y ∀α. f α → α ∀α. f α → α . Esto se parece a la definición de un comonad:

class Functor f ⇒ Comonad f where coreturn ∷ f α → α cojoin ∷ f α → f (f α)

Entonces, un comonad es entonces una coalgebra en una categoría de endofunctores.

Comenzaré con cosas que obviamente están relacionadas con la programación y luego agregaré algunas cosas de matemáticas para mantenerlas tan concretas y realistas como pueda.

Citemos algunos informáticos sobre coinducción ...

http://www.cs.umd.edu/~micinski/posts/2012-09-04-on-understanding-coinduction.html

La inducción se trata de datos finitos, la coinducción se trata de datos infinitos.

El ejemplo típico de datos infinitos es el tipo de una lista perezosa (una secuencia). Por ejemplo, digamos que tenemos el siguiente objeto en la memoria:

let (pi : int list) = (* some function which computes the digits of π. *)

¡La computadora no puede contener todo π, porque solo tiene una cantidad finita de memoria! Pero lo que puede hacer es mantener un programa finito, que producirá cualquier expansión arbitrariamente larga de π que desee. Siempre y cuando solo uses partes finitas de la lista, puedes calcular con esa lista infinita todo lo que necesites.

Sin embargo, considere el siguiente programa:

let print_third_element (k : int list) = match k with | _ :: _ :: thd :: tl -> print thd print_third_element pi

Este programa debe imprimir el tercer dígito de pi. Pero en algunos idiomas, cualquier argumento a una función se evalúa antes de pasar a una función (evaluación estricta, no perezosa). Si usamos esta orden de reducción, entonces nuestro programa anterior se ejecutará para siempre calculando los dígitos de pi antes de que pueda pasar a nuestra función de impresora (lo que nunca sucede). Dado que la máquina no tiene memoria infinita, el programa eventualmente se quedará sin memoria y se bloqueará. Este podría no ser el mejor orden de evaluación.

http://adam.chlipala.net/cpdt/html/Coinductive.html

En los lenguajes de programación perezosos funcionales como Haskell, las estructuras de datos infinitas están en todas partes. Las listas infinitas y los tipos de datos más exóticos proporcionan abstracciones convenientes para la comunicación entre las partes de un programa. Lograr una comodidad similar sin infinitas estructuras perezosas requeriría, en muchos casos, inversiones acrobáticas del flujo de control.

http://www.alexandrasilva.org/#/talks.html

Relacionar el contexto matemático ambiental con las tareas de programación habituales.

¿Qué es "un álgebra"?

Las estructuras algebraicas generalmente se ven como:

  1. Cosas
  2. Lo que las cosas pueden hacer

Esto debería sonar como objetos con 1. propiedades y 2. métodos. O incluso mejor, debe sonar como firmas de tipo.

Los ejemplos matemáticos estándar incluyen monoid ⊃ grupo ⊃ espacio-vector ⊃ "un álgebra". Los monoides son como autómatas: secuencias de verbos (por ejemplo, fghhnothing.fgf ). Un registro de git que siempre agrega el historial y nunca lo elimina sería un monoide pero no un grupo. Si agrega inversos (por ejemplo, números negativos, fracciones, raíces, eliminación del historial acumulado, destrozando un espejo roto), obtiene un grupo.

Los grupos contienen cosas que pueden sumarse o restarse juntas. Por ejemplo, la Duration s se puede agregar juntos. (Pero las Date no pueden). Las duraciones viven en un espacio vectorial (no solo un grupo) porque también se pueden escalar por números externos. (Una firma de tipo de scaling :: (Number,Duration) → Duration .)

Algebras ⊂ los espacios vectoriales pueden hacer otra cosa: hay algunos m :: (T,T) → T Llama a esto "multiplicación" o no, porque una vez que dejas Integers es menos obvio que "multiplicación" (o "exponentiation" ) debería ser.

(Esta es la razón por la cual las personas buscan las propiedades universales (de la categoría de la teoría): para decirles qué debe hacer o cómo debe ser la multiplicación

)

Algebras → Coalgebras

La multiplicación múltiple es más fácil de definir de una manera que parece no arbitraria, que la multiplicación, porque para pasar de T → (T,T) puedes repetir el mismo elemento. ("mapa diagonal" - como matrices diagonales / operadores en teoría espectral)

Counit suele ser la traza (suma de entradas diagonales), aunque nuevamente lo importante es lo que hace su counit; trace es solo una buena respuesta para las matrices.

La razón para mirar un espacio dual , en general, es porque es más fácil pensar en ese espacio. Por ejemplo, a veces es más fácil pensar en un vector normal que en el plano al que es normal, pero puedes controlar los planos (incluidos los hiperplanos) con vectores (y ahora estoy hablando del vector geométrico familiar, como en un trazador de rayos) .

Domar (des) datos estructurados

Los matemáticos podrían estar modelando algo divertido como TQFT''s , mientras que los programadores tienen que luchar con

  • fechas / horas ( + :: (Date,Duration) → Date ),
  • lugares ( Paris ≠ (+48.8567,+2.3508) ! Es una forma, no un punto),
  • JSON no estructurado que se supone que es consistente en algún sentido,
  • XML incorrecto pero cercano,
  • Datos GIS increíblemente complejos que deben satisfacer un montón de relaciones sensibles,
  • Expresiones regulares que significan algo para ti, pero significan mucho menos para Perl.
  • CRM que debe contener todos los números de teléfono del ejecutivo y las ubicaciones de las villas, los nombres de su (ahora ex) esposa e hijos, cumpleaños y todos los regalos anteriores, cada uno de los cuales debe satisfacer relaciones "obvias" (obvias para el cliente) que son increíblemente difícil de codificar,
  • .....

Los informáticos, cuando hablan de coalgebras, suelen tener en mente operaciones de configuración, como el producto cartesiano. Creo que esto es lo que la gente quiere decir cuando dice "Las algebras son coalgebras en Haskell".Pero en la medida en que los programadores tienen que modelar tipos de datos complejos como Place, Date/Timey Customer—y hacer que esos modelos se parezcan al mundo real (o al menos la visión del mundo real del usuario final) como sea posible— podría ser útil más allá del único mundo fijo.

F-álgebras y F-coalgebras son estructuras matemáticas que son instrumentales en el razonamiento sobre tipos inductivos (o tipos recursivos ).

F-álgebras

Empezaremos primero con F-álgebras. Intentaré ser lo más simple posible.

Supongo que sabes lo que es un tipo recursivo. Por ejemplo, este es un tipo para una lista de enteros:

data IntList = Nil | Cons (Int, IntList)

Es obvio que es recursivo, de hecho, su definición se refiere a sí misma. Su definición consiste en dos constructores de datos, que tienen los siguientes tipos:

Nil :: () -> IntList Cons :: (Int, IntList) -> IntList

Tenga en cuenta que he escrito tipo Nil como () -> IntList , no simplemente IntList . De hecho, estos son tipos equivalentes desde el punto de vista teórico, porque () tipo tiene solo un habitante.

Si escribimos las firmas de estas funciones de una manera más teórica, obtendremos

Nil :: 1 -> IntList Cons :: Int × IntList -> IntList

donde 1 es un conjunto de unidades (conjunto con un elemento) y la operación A × B es un producto cruzado de dos conjuntos A y B (es decir, un conjunto de pares (a, b) donde a pasa por todos los elementos de A y b va a través de todos los elementos de B ).

Unión desunida de dos conjuntos A y B es un conjunto A | B A | B que es una unión de conjuntos {(a, 1) : a in A} y {(b, 2) : b in B} . Esencialmente, es un conjunto de todos los elementos de A y B , pero con cada uno de estos elementos ''marcados'' como pertenecientes a A o B , así que cuando seleccionamos cualquier elemento de A | B A | B sabremos de inmediato si este elemento proviene de A o de B

Podemos ''unir'' las funciones Nil y Cons , por lo que formarán una sola función trabajando en un conjunto 1 | (Int × IntList) 1 | (Int × IntList) :

Nil|Cons :: 1 | (Int × IntList) -> IntList

De hecho, si la función Nil|Cons se aplica a () valor (que, obviamente, pertenece al conjunto 1 | (Int × IntList) ), entonces se comporta como si fuera Nil ; si Nil|Cons se aplica a cualquier valor de tipo (Int, IntList) (dichos valores también se encuentran en el conjunto 1 | (Int × IntList) , se comporta como Cons .

Ahora considere otro tipo de datos:

data IntTree = Leaf Int | Branch (IntTree, IntTree)

Cuenta con los siguientes constructores:

Leaf :: Int -> IntTree Branch :: (IntTree, IntTree) -> IntTree

que también se puede unir en una función:

Leaf|Branch :: Int | (IntTree × IntTree) -> IntTree

Se puede ver que estas dos funciones joined tienen un tipo similar: ambas parecen

f :: F T -> T

donde F es un tipo de transformación que toma nuestro tipo y da un tipo más complejo, que consiste en x y | Operaciones, usos de T y posiblemente otros tipos. Por ejemplo, para IntList e IntTree F ve como sigue:

F1 T = 1 | (Int × T) F2 T = Int | (T × T)

Podemos notar inmediatamente que cualquier tipo algebraico puede escribirse de esta manera. De hecho, es por eso que se les llama ''algebraicos'': consisten en una cantidad de ''sumas'' (uniones) y ''productos'' (productos cruzados) de otros tipos.

Ahora podemos definir F-algebra. El álgebra F es solo un par (T, f) , donde T es algún tipo y f es una función de tipo f :: FT -> T En nuestros ejemplos, las F-álgebras son (IntList, Nil|Cons) y (IntTree, Leaf|Branch) . Tenga en cuenta, sin embargo, que a pesar de que el tipo de función f es el mismo para cada F, T f pueden ser arbitrarios. Por ejemplo, (String, g :: 1 | (Int x String) -> String) o (Double, h :: Int | (Double, Double) -> Double) para algunos g y h también son F-álgebras para los correspondientes F.

Luego podemos introducir homomorfismos de álgebra F y luego álgebras F iniciales , que tienen propiedades muy útiles. De hecho, (IntList, Nil|Cons) es un álgebra inicial F1, y (IntTree, Leaf|Branch) es un álgebra F2 inicial. No presentaré definiciones exactas de estos términos y propiedades ya que son más complejas y abstractas de lo necesario.

No obstante, el hecho de que, digamos, (IntList, Nil|Cons) es un álgebra F, nos permite definir una función de tipo fold en este tipo. Como saben, fold es un tipo de operación que transforma algunos tipos de datos recursivos en un valor finito. Por ejemplo, podemos plegar una lista de enteros en un solo valor que es una suma de todos los elementos de la lista:

foldr (+) 0 [1, 2, 3, 4] -> 1 + 2 + 3 + 4 = 10

Es posible generalizar dicha operación en cualquier tipo de datos recursivo.

La siguiente es una firma de la función foldr :

foldr :: ((a -> b -> b), b) -> [a] -> b

Tenga en cuenta que he usado llaves para separar los dos primeros argumentos de la última. Esta no es una función foldr real, pero es isomorfa (es decir, puede obtener fácilmente una de la otra y viceversa). Parcialmente aplicado foldr tendrá la siguiente firma:

foldr ((+), 0) :: [Int] -> Int

Podemos ver que esta es una función que toma una lista de enteros y devuelve un solo entero. Vamos a definir dicha función en términos de nuestro tipo IntList .

sumFold :: IntList -> Int sumFold Nil = 0 sumFold (Cons x xs) = x + sumFold xs

Vemos que esta función consta de dos partes: la primera parte define el comportamiento de esta función en la parte IntList de IntList , y la segunda parte define el comportamiento de la función en la parte Cons .

Ahora supongamos que no estamos programando en Haskell, sino en un lenguaje que permite el uso de tipos algebraicos directamente en firmas de tipos (bueno, técnicamente, Haskell permite el uso de tipos algebraicos a través de tuplas y Either ab tipos de datos, pero esto llevará a una información innecesaria). Considere una función:

reductor :: () | (Int × Int) -> Int reductor () = 0 reductor (x, s) = x + s

Se puede ver que el reductor es una función de tipo F1 Int -> Int , ¡como en la definición de F-algebra! De hecho, el par (Int, reductor) es un álgebra de F1.

Debido a que IntList es un álgebra inicial F1, para cada tipo T y para cada función r :: F1 T -> T existe una función, llamada catamorfismo para r , que convierte IntList en T , y dicha función es única. De hecho, en nuestro ejemplo se sumFold un catamorfismo para el reductor . Note cómo reductor y sumFold son similares: ¡tienen casi la misma estructura! En la definición de reductor s uso de parámetros (el tipo del cual corresponde a T ) corresponde al uso del resultado del cálculo de sumFold xs en la definición de sumFold .

Solo para hacerlo más claro y ayudarlo a ver el patrón, aquí hay otro ejemplo, y nuevamente comenzamos desde la función de plegado resultante. Considere la función de append que adjunta su primer argumento al segundo:

(append [4, 5, 6]) [1, 2, 3] = (foldr (:) [4, 5, 6]) [1, 2, 3] -> [1, 2, 3, 4, 5, 6]

Así se ve en nuestra IntList :

appendFold :: IntList -> IntList -> IntList appendFold ys () = ys appendFold ys (Cons x xs) = x : appendFold ys xs

Nuevamente, tratemos de escribir el reductor:

appendReductor :: IntList -> () | (Int × IntList) -> IntList appendReductor ys () = ys appendReductor ys (x, rs) = x : rs

appendFold es un catamorfismo para appendReductor que transforma IntList en IntList .

Así que, esencialmente, las F-álgebras nos permiten definir ''pliegues'' en estructuras de datos recursivas, es decir, operaciones que reducen nuestras estructuras a algún valor.

F-coalgebras

F-coalgebras se denominan término ''dual'' para F-algebras. Nos permiten definir unfolds para tipos de datos recursivos, es decir, una forma de construir estructuras recursivas a partir de algún valor.

Supongamos que tiene el siguiente tipo:

data IntStream = Cons (Int, IntStream)

Este es un flujo infinito de enteros. Su único constructor tiene el siguiente tipo:

Cons :: (Int, IntStream) -> IntStream

O bien, en términos de conjuntos.

Cons :: Int × IntStream -> IntStream

Haskell le permite establecer patrones en los constructores de datos, por lo que puede definir las siguientes funciones trabajando en IntStream s:

head :: IntStream -> Int head (Cons (x, xs)) = x tail :: IntStream -> IntStream tail (Cons (x, xs)) = xs

Naturalmente, puede ''unir'' estas funciones en una sola función de tipo IntStream -> Int × IntStream :

head&tail :: IntStream -> Int × IntStream head&tail (Cons (x, xs)) = (x, xs)

Observe cómo el resultado de la función coincide con la representación algebraica de nuestro tipo IntStream . Lo mismo puede hacerse para otros tipos de datos recursivos. Tal vez ya hayas notado el patrón. Me refiero a una familia de funciones de tipo.

g :: T -> F T

donde T es algún tipo. A partir de ahora definiremos

F1 T = Int × T

Ahora, F-coalgebra es un par (T, g) , donde T es un tipo y g es una función de tipo g :: T -> FT . Por ejemplo, (IntStream, head&tail) es un F1-coalgebra. Una vez más, al igual que en F-álgebras, g y T pueden ser arbitrarias, por ejemplo, (String, h :: String -> Int x String) también es una F1-coalgebra para algunos h.

Entre todas las F-coalgebras hay las llamadas F-coalgebras terminales , que son duales a las F-álgebras iniciales. Por ejemplo, IntStream es un terminal F-coalgebra. Esto significa que para cada tipo T y para cada función p :: T -> F1 T existe una función, llamada anamorphism , que convierte T en IntStream , y dicha función es única.

Considere la siguiente función, que genera un flujo de enteros sucesivos a partir de uno dado:

nats :: Int -> IntStream nats n = Cons (n, nats (n+1))

Ahora inspeccionemos una función natsBuilder :: Int -> F1 Int , es decir, natsBuilder :: Int -> Int × Int :

natsBuilder :: Int -> Int × Int natsBuilder n = (n, n+1)

Una vez más, podemos ver cierta similitud entre nats y natsBuilder . Es muy similar a la conexión que hemos observado con reductores y pliegues anteriores. nats es un natsBuilder para natsBuilder .

Otro ejemplo, una función que toma un valor y una función y devuelve un flujo de aplicaciones sucesivas de la función al valor:

iterate :: (Int -> Int) -> Int -> IntStream iterate f n = Cons (n, iterate f (f n))

Su función constructora es la siguiente:

iterateBuilder :: (Int -> Int) -> Int -> Int × Int iterateBuilder f n = (n, f n)

Entonces iterate es un iterateBuilder para iterateBuilder .

Conclusión

Entonces, en resumen, las F-álgebras permiten definir los pliegues, es decir, las operaciones que reducen la estructura recursiva en un solo valor, y las F-coalgebras permiten hacer lo contrario: construir una estructura [potencialmente] infinita a partir de un solo valor.

De hecho en Haskell coinciden F-algebras y F-coalgebras. Esta es una propiedad muy agradable que es consecuencia de la presencia del valor "inferior" en cada tipo. Así que en Haskell se pueden crear tanto pliegues como despliegues para cada tipo recursivo. Sin embargo, el modelo teórico detrás de esto es más complejo que el que he presentado anteriormente, por lo que deliberadamente lo he evitado.

Espero que esto ayude.

Revisando el artículo del tutorial Un tutorial sobre (co) álgebras y (co) inducción debería darle una idea sobre el co-álgebra en ciencias de la computación.

A continuación hay una cita para convencerte,

En términos generales, un programa en algún lenguaje de programación manipula datos. Durante el desarrollo de la informática en las últimas décadas, quedó claro que una descripción abstracta de estos datos es deseable, por ejemplo, para garantizar que el programa de uno no dependa de la representación particular de los datos sobre los que opera. Además, tal abstracción facilita las pruebas de corrección.
Este deseo condujo al uso de métodos algebraicos en ciencias de la computación, en una rama llamada especificación algebraica o teoría abstracta del tipo de datos. El objeto de estudio son los tipos de datos en sí mismos, utilizando nociones de técnicas que son familiares del álgebra. Los tipos de datos utilizados por los científicos informáticos a menudo se generan a partir de una colección dada de operaciones (constructor), y es por esta razón que la "inicialidad" de álgebras juega un papel tan importante.
Las técnicas algebraicas estándar han demostrado ser útiles para capturar varios aspectos esenciales de las estructuras de datos utilizadas en la informática. Pero resultó difícil describir algebraicamente algunas de las estructuras dinámicas inherentes que ocurren en la computación. Tales estructuras usualmente involucran una noción de estado, que puede ser transformada de varias maneras. Los enfoques formales de tales sistemas dinámicos basados ​​en estado generalmente hacen uso de autómatas o sistemas de transición, como referencias tempranas clásicas.
Durante la última década, la idea creció gradualmente de que tales sistemas basados ​​en el estado no deberían describirse como álgebras, sino como las llamadas co-álgebras. Estos son el dual formal de álgebras, de una manera que se hará precisa en este tutorial. La propiedad dual de "inicialidad" para las álgebras, es decir, la finalidad, resultó crucial para tales co-álgebras. Y el principio de razonamiento lógico que se necesita para tales co-álgebras finales no es la inducción sino la co-inducción.

Preludio, sobre la teoría de la categoría. La teoría de categorías debería ser renombrada como teoría de los funtores. Como categorías son lo que hay que definir para definir los funtores. (Además, los funtores son lo que uno debe definir para definir transformaciones naturales).

¿Qué es un funtor? Es una transformación de un conjunto a otro que preserva su estructura. (Para más detalles hay muchas buenas descripciones en la red).

¿Qué es un álgebra F? Es el álgebra del functor. Es solo el estudio de la propiedad universal del functor.

¿Cómo se puede vincular a la informática? El programa se puede ver como un conjunto estructurado de información. La ejecución del programa corresponde a la modificación de este conjunto estructurado de información. Suena bien que la ejecución debe preservar la estructura del programa. Luego, la ejecución se puede ver como la aplicación de un functor sobre este conjunto de información. (El que define el programa).

¿Por qué F-co-álgebra? Los programas son duales por esencia, ya que se describen por información y actúan en consecuencia. Luego, principalmente la información que compone el programa y los modifica se puede ver de dos maneras.

  • Datos que pueden definirse como la información que está siendo procesada por el programa.
  • Estado que puede definirse como la información que comparte el programa.

Entonces en esta etapa, me gustaría decir eso,

  • El álgebra F es el estudio de la transformación funcional que actúa sobre el universo de Data (como se ha definido aquí).
  • F-co-álgebras es el estudio de la transformación funcional que actúa sobre el Universo del Estado (como se ha definido aquí).

Durante la vida de un programa, los datos y el estado coexisten, y se completan entre sí. Son duales