haskell - for - ¿Dónde encajan los valores en la Categoría de Hask?

category theory for programmers (5)

Entonces tenemos la Categoría de Hask, donde:

Los tipos son los objetos de la categoría
Las funciones son los morfismos de un objeto a otro en la categoría.

Del mismo modo para Functor tenemos:

un constructor de tipo como el mapeo de objetos de una categoría a otra
fmap para el mapeo de morfismos de una categoría a otra.

Ahora, cuando escribimos un programa, básicamente transformamos valores (no tipos) y parece que la Categoría de Hask no habla de valores en absoluto. Intenté ajustar los valores en toda la ecuación y obtuve la siguiente observación:

Cada Tipo es una categoría en sí misma. Ej: Int es una categoría de todos los enteros.
Las funciones de un valor a otro del mismo tipo son el morfismo de la categoría. Ej: Int -> Int
Las funciones de un valor a otro de diferente tipo son un functor para asignar valores de un tipo a otro.

Ahora mi pregunta es: ¿los valores incluso tienen sentido en la categoría de Hask (o en la teoría general de categorías)? Si es así, cualquier referencia para leer sobre eso O si no, entonces cualquier razón para eso.

Espero que la pregunta tenga sentido :)

(Usaré palabras con su significado de matemáticas / teoría de categorías en lugar de programación, a menos que lo mark it as code ).

Una categoría a la vez

Una de las grandes ideas de la teoría de categorías es tratar grandes cosas complejas como un punto, por lo que, para formar la categoría set / group / ring / class / de todos los enteros, se considera un punto único cuando se está pensando en la categoría Hask .

Del mismo modo, podría tener una función muy complicada en enteros, pero solo se considera un elemento único (punto / flecha) de una colección (conjunto / clase) de morfismos.

Lo primero que haces en la teoría de categorías es ignorar los detalles. Entonces, a la categoría Hask no le importa que Int se pueda considerar una categoría, eso está en un nivel diferente. Int es solo un punto (objeto) en Hask.

Un nivel abajo

Cada monoide es una categoría con un objeto. Usemos eso.

¿Cómo son los enteros una categoría?

Hay más de una respuesta a esto (ya que los enteros son un monoide bajo adición y un monoide bajo multiplicación). Hagamos además:

Puede considerar los enteros como una categoría con un solo objeto, y los morfismos son funciones como (+1), (+2), (restar 4).

Tienes que tener en mente que estoy considerando el número entero 7 como el número 7 pero usando la representación (+7) para que parezca una categoría. Las leyes de la teoría de categorías deliberadamente no dicen que tus morfismos tienen que ser funciones, pero es más claro que algo es una categoría si tiene la estructura de un conjunto de funciones que contienen identidad y están cerradas bajo composición.

Cualquier monoide hace una categoría de objeto único de la misma manera que lo hemos hecho con los enteros.

Functores de los enteros?

Una función f de los enteros como categoría bajo la operación + , para algún otro tipo con una operación £ que forma una categoría solo podría ser un funtor si tuvieras f(x+y) = f(x) £ f(y) . (Esto se llama homomorfismo monoide). La mayoría de las funciones no son morfismos.

Ejemplo de morfismo

String son un monoide bajo ++ , entonces son una categoría.

len :: String -> Int len = length

len es un morfismo monoide de String a Int , porque len (xs ++ ys) = len xs + len ys , por lo que si estás considerando ( String , ++ ) y ( Int , + ) como categoría, len es un funtor .

Ejemplo de no morfismo

( Bool , || ) es un monoide, con False como identidad, por lo que es una categoría de un solo objeto. La función

quiteLong :: String -> Bool quiteLong xs = length xs > 10

no es un morfismo porque quiteLong "Hello " es False y quiteLong "there!" también es False , pero quiteLong ("Hello " ++ "there!") es True y False || False False || False no es True .

Porque quiteLong no es un morfismo, tampoco es un functor.

¿Cuál es tu punto, Andrew?

Mi punto es que algunos tipos de Haskell se pueden considerar categorías, pero no todas las funciones entre ellos son morhpisms.

No pensamos en las categorías en niveles diferentes al mismo tiempo (a menos que use ambas categorías para algún propósito extraño), y deliberadamente no hay interacción teórica entre los niveles, porque deliberadamente no hay detalles sobre los objetos y morfismos.

Esto se debe en parte a que la teoría de categorías despegó en matemáticas para proporcionar un lenguaje que describiera la encantadora interacción de la teoría de Galois entre grupos / subgrupos finitos y extensiones de campo / campo, dos estructuras aparentemente completamente diferentes que resultan estar estrechamente relacionadas. Más tarde, la teoría de la homología / homotopía hizo funtores entre espacios y grupos topológicos que resultan ser fascinantes y útiles, pero el punto principal es que los objetos y los morfismos pueden ser muy diferentes entre sí en las dos categorías de un funtor .

(Normalmente, la teoría de categorías entra en Haskell en forma de un funtor de Hask a Hask, por lo que en la práctica en la programación funcional las dos categorías son las mismas).

Entonces ... ¿cuál es exactamente la respuesta a la pregunta original?

Cada Tipo es una categoría en sí misma. Ej: Int es una categoría de todos los enteros.

Si piensas en ellos de maneras particulares. Ver la respuesta de PhilipJF para más detalles.

Las funciones de un valor a otro del mismo tipo son el morfismo de la categoría. Ej: Int -> Int

Creo que confundiste los dos niveles. Las funciones pueden ser morfismos en Hask, pero no todas las funciones Int -> Int son Functors bajo la estructura de suma, por ejemplo fx = 2 * x + 10 no es un funtor entre Int e Int, entonces no es un morfismo de categoría (otra manera) de decir functor) de ( Int , + ) a ( Int , + ) pero es un morfismo Int -> Int en la categoría Hask.

Las funciones de un valor a otro de diferente tipo son un functor para asignar valores de un tipo a otro.

No, no todas las funciones son funtores, por ejemplo, quiteLong no lo es.

¿Los valores incluso tienen sentido en la Categoría de Hask (o en la teoría general de categorías)?

Las categorías no tienen valores en la teoría de categorías, solo tienen objetos y morfismos, que se tratan como vértices y bordes dirigidos. Los objetos no tienen que tener valores, y los valores no son parte de la teoría de categorías.

Hay varias formas de poner las cosas en términos de categorías. Especialmente lenguajes de programación, que resultan ser construcciones muy ricas.

Si elegimos la categoría Hask, solo estamos estableciendo un nivel de abstracción. Un nivel donde no es tan cómodo hablar de valores.

Sin embargo, las constantes se pueden modelar en Hask como una flecha desde el objeto terminal () al tipo correspondiente. Entonces, por ejemplo:

Verdadero: () -> Bool
''a'': () -> Char

Puede consultar: Barr, Wells - Teoría de categorías para informática, sección 2.2.

Si bien hay algunas otras respuestas bastante maravillosas aquí, todos se pierden su primera pregunta de alguna manera. Para ser claros, los valores simplemente no existen y no tienen significado en la categoría Hask. Eso no es de lo que Hask está para hablar.

Lo anterior parece un poco tonto de decir o sentir, pero lo menciono porque es importante tener en cuenta que la teoría de categorías proporciona solo una lente para examinar las interacciones y estructuras mucho más complejas disponibles en algo tan sofisticado como un lenguaje de programación. No es fructífero esperar que toda esa estructura sea subsumida por la noción más bien simple de una categoría. [1]

Otra forma de decir esto es que estamos tratando de analizar un sistema complejo y a veces es útil verlo como una categoría para buscar patrones interesantes. Es esta mentalidad la que nos permite introducir Hask, verificar que realmente forme una categoría, notar que Maybe parece comportarse como un Functor, y luego usar todos esos mecanismos para escribir las condiciones de coherencia.

fmap id = id fmap f . fmap g = fmap (f . g)

Estas reglas tendrían sentido independientemente de si presentamos Hask, pero al verlas como simples consecuencias de una estructura simple que podemos descubrir dentro de Haskell comprendemos su importancia.

Como nota técnica, la totalidad de esta respuesta asume que Hask es en realidad "platónico" Hask, es decir, podemos ignorar el fondo ( undefined y sin terminación) tanto como queramos. Sin eso, casi todo el argumento se desmorona un poco.

Examinemos esas leyes más de cerca ya que parecen estar en contra de mi afirmación inicial: obviamente están operando en el nivel de valor, pero "los valores no existen en Hask", ¿verdad?

Bueno, una respuesta es mirar más de cerca qué es un functor categórico. Explícitamente, es un mapeo entre dos categorías (digamos C y D) que lleva los objetos de C a los objetos de D y las flechas de C a las flechas de D. Vale la pena señalar que, en general, estos "mapeos" no son flechas categóricas; una relación entre las categorías y no necesariamente comparte en estructura con las categorías.

Esto es importante porque incluso teniendo en cuenta Haskell Functor s, endofunctors en Hask, tenemos que tener cuidado. En Hask, los objetos son tipos Haskell y las flechas son funciones Haskell entre esos tipos.

Miremos Maybe otra Maybe . Si va a ser un endofunctor en Hask, entonces necesitamos una forma de llevar todos los tipos en Hask a otros tipos en Hask. Este mapeo no es una función de Haskell aunque pueda parecer una: pure :: a -> Maybe a no califica porque opera en el nivel de valor . En cambio, nuestro mapeo de objetos es Maybe : para cualquier tipo a podemos formar el tipo Maybe a .

Esto ya destaca el valor de trabajar en Hask sin valores --- realmente queremos aislar una noción de Functor que no dependa de pure .

Desarrollaremos el resto de Functor examinando el mapeo de flechas de nuestro Maybe endofunctor. Aquí necesitamos una forma de asignar las flechas de Hask a las flechas de Hask. Supongamos por ahora que esta no es una función de Haskell, no tiene que ser así, así que para enfatizarla la escribiremos de manera diferente. Si f es una función de Haskell a -> b entonces Tal vez [ f ] es alguna otra función de Haskell Maybe a -> Maybe b .

Ahora, es difícil no adelantarse y simplemente comenzar a llamar Maybe [ f ] " fmap f ", pero podemos hacer un poco más de trabajo antes de dar ese salto. Tal vez [ f ] necesita tener ciertas condiciones de coherencia. En particular, para cualquier tipo a en Hask tenemos una flecha de id. En nuestro metalenguaje podríamos llamarlo id [ a ] y sabemos que también se conoce con el nombre de Haskell id :: a -> a . En total, podemos usar estos para indicar las condiciones de coherencia del endofunctor:

Para todos los objetos en Hask a , tenemos que Maybe [id [ a ]] = id [ Maybe a ]. Para cualquier dos flechas en Hask f g , tenemos que Maybe [ f . g f . g ] = Tal vez [ f ]. Tal vez [ g ].

El paso final es notar que Maybe [_] resulta ser realizable como una función Haskell en sí misma como un valor del objeto Hask for all forall ab . (a -> b) -> (Maybe a -> Maybe b) forall ab . (a -> b) -> (Maybe a -> Maybe b) . Eso nos da Functor .

Si bien lo anterior era bastante técnico y complejo, hay un punto importante para mantener las nociones de Hask y los endofunctors categóricos directamente y separados de su instanciación de Haskell. En particular, podemos descubrir toda esta estructura sin introducir la necesidad de que fmap exista como una verdadera función Haskell. Hask es una categoría sin introducir nada en absoluto en el nivel de valor.

Ahí es donde vive el verdadero corazón de ver a Hask como una categoría. La notación que identifica endofunctors en Hask con Functor requiere mucha más borrosidad de línea.

Esta línea borrosa se justifica porque Hask tiene exponenciales . Esta es una forma engañosa de decir que hay una unificación entre paquetes completos de flechas categóricas y objetos particulares y especiales en Hask.

Para ser más explícitos, sabemos que para cualquier dos objetos de Hask, digamos b , podemos hablar de las flechas entre esos dos objetos, a menudo denotados como Hask ( a , b ). Esto es solo un conjunto matemático, pero sabemos que hay otro tipo en Hask que está estrechamente relacionado con Hask ( a , b ): (a -> b) !

Entonces esto es extraño.

Originalmente, declare que los valores generales de Haskell no tienen absolutamente ninguna representación en la presentación categórica de Hask. Luego, pasé a demostrar que podemos hacer mucho con Hask utilizando solo sus nociones categóricas y sin incluir esas piezas dentro de Haskell como valores.

Pero ahora estoy notando que los valores de un tipo como a -> b realidad existen como todas las flechas en el conjunto metalingüístico Hask ( a , b ). Eso es todo un truco y es exactamente esta confusión metalingüística lo que hace que las categorías con exponenciales sean tan interesantes.

Sin embargo, podemos hacerlo un poco mejor! Hask también tiene un objeto terminal. Podemos hablar de esto metalingüísticamente llamándolo 0, pero también lo conocemos como el tipo Haskell () . Si observamos cualquier objeto Hask, sabremos que hay un conjunto completo de flechas categóricas en Hask ( () , a ). Además, sabemos que estos corresponden a los valores del tipo () -> a . Finalmente, dado que sabemos que dada cualquier función f :: () -> a podemos obtener inmediatamente a a mediante la aplicación () uno puede querer decir que las flechas categóricas en Hask ( () , a ) son exactamente los valores Haskell de escribe a .

Lo cual debería ser completamente confuso o increíblemente alucinante.

Voy a terminar esto de una manera un tanto filosófica al mantener mi declaración inicial: Hask no habla de los valores de Haskell en absoluto. Realmente no es una categoría pura: las categorías son interesantes precisamente porque son muy simples y, por lo tanto, no necesitan todas estas nociones typeOf de tipos y valores y typeOf inclusión y similares.

Pero también, quizás deficientemente, mostré que incluso como estrictamente solo una categoría , Hask tiene algo que se ve muy, muy similar a todos los valores de Haskell: las flechas de Hask ( () , a ) para cada objeto Hask a .

Filosóficamente, podríamos argumentar que estas flechas no son realmente los valores de Haskell que estamos buscando; son solo simulacros, burlas categóricas. Podría argumentar que son cosas diferentes, pero que simplemente están en correspondencia uno a uno con los valores de Haskell.

De hecho, creo que es una idea realmente importante a tener en cuenta. Estas dos cosas son diferentes, simplemente se comportan de manera similar.

Muy similarmente Cualquier categoría te permite componer flechas, así que supongamos que escogemos alguna flecha en Hask ( a , b ) y alguna flecha en Hask ( () , a ). Si combinamos estas flechas con la composición de categoría obtenemos una flecha en Hask ( () , b ). Volviendo todo esto a la cabeza, podríamos decir que lo que acabo de hacer fue encontrar un valor de tipo a -> b , un valor de tipo a , y luego combinarlos para producir un valor de tipo b .

En otras palabras, si miramos hacia los lados podemos ver la composición de flecha categórica como una forma generalizada de aplicación de función.

Esto es lo que hace que categorías como Hask sean tan interesantes. En general, este tipo de categorías se denominan categorías cerradas cartesianas o CCC. Debido a que tienen tanto objetos iniciales como exponenciales (que también requieren productos), tienen estructuras que modelan completamente el cálculo lambda tipado.

Pero todavía no tienen valores .

[1] Si estás leyendo esto antes de leer el resto de mi respuesta, sigue leyendo. Resulta que si bien es absurdo esperar que eso suceda, realmente lo hace. Si estás leyendo esto después de leer toda mi respuesta, solo reflexionemos sobre cuán geniales son los CCC.

Cualquier categoría con un objeto terminal (o con el objeto terminal * s *) tiene los denominados elementos globales (o puntos , o constantes , también en Wikipedia , se pueden encontrar más, por ejemplo, en el libro de Awoday sobre Teoría de categorías, ver 2.3 Elementos generalizados ) de objetos que podemos llamar valores de estos objetos aquí, tomando elementos globales como una noción categórica natural y universal de "valores".

Por ejemplo, Set tiene elementos habituales (de conjuntos, objetos de Set ) como elementos globales, lo que significa que los elementos de cualquier conjunto A pueden verse como diferentes funciones (morfismos de Set ) {⋆} → A desde un conjunto de unidades {⋆} a este conjunto A Para un conjunto finito A con |A| = n |A| = n hay n tales morfismos, para un conjunto vacío {} no hay tales morfismos {⋆} → {} en Set , por lo que {} "no tiene elementos" y |{}| = 0 |{}| = 0 , para singleton establece {⋆} ≊ {+} únicamente, de modo que |{⋆}| = |{+}| = 1 |{⋆}| = |{+}| = 1 |{⋆}| = |{+}| = 1 , y así sucesivamente. Los elementos o "valores" de los conjuntos son realmente funciones simples de un conjunto único ( 1 , objeto terminal en Set ), ya que hay un isomorfismo A ≊ Hom(1, A) en Set (que es CCC , por lo que Hom es interno aquí y Hom(1, A) es un objeto).

De modo que los elementos globales son una generalización de esta noción de elementos en Set a cualquier categoría con objetos terminales. Se puede generalizar más con elementos generalizados (en una categoría de conjuntos, posets o espacios, los morfismos están determinados por acciones en puntos, pero no siempre es el caso en una categoría general). En general, una vez que convertimos los "valores" (elementos, puntos, constantes, términos) en flechas de una categoría en cuestión, podemos razonar sobre ellos utilizando el lenguaje de esta categoría en particular.

Del mismo modo, en Hask tenemos, por ejemplo, true como ⊤ → Bool y false como ⊤ → Bool :

true :: () -> Bool true = const True false :: () -> Bool false = const Frue

true ≠ false en un sentido habitual , también, tenemos una familia de ⊥ ''como ⊤ → Bool ( undefined , error "..." , fix , recursión general, etc.):

bottom1 :: () -> Bool bottom1 = const undefined bottom2 :: () -> Bool bottom2 = const $ error "..." bottom3 :: () -> Bool bottom3 = const $ fix id bottom4 :: () -> Bool bottom4 = bottom4 bottom5 :: () -> Bool bottom5 = const b where b = b ...

⊥ ≠ false ≠ true y esto es todo, no podemos encontrar ningún otro morfismo de la forma ⊤ → Bool , por lo que ⊥ , false y true son los únicos valores de Bool que se pueden distinguir de forma ⊤ → Bool . Tenga en cuenta que en Hask cualquier objeto tiene valores, es decir, que está habitado, ya que siempre hay morfismos ⊤ → A para cualquier tipo A , hace que Hask sea diferente de Set o cualquier otro CCC no trivial (su lógica interna es un poco aburrida, esto es lo que es Rápido y Loose Reasoning es moralmente correcto , tenemos que buscar un subconjunto de Haskell que tenga un buen CCC con una lógica sensata).

Además, en los valores de la teoría de tipos se representan sintácticamente como términos que nuevamente tienen una semántica categórica similar.

Y si hablamos de BiCCC "platónico" (es decir, total, BiCCC ), entonces aquí hay una prueba trivial de A ≊ Hom(1, A) en Agda (que capta bien los rasgos platónicos):

module Values where open import Function open import Data.Unit open import Data.Product open import Relation.Binary.PropositionalEquality _≊_ : Set → Set → Set A ≊ B = ∃ λ (f : A → B) → ∃ λ (f⁻¹ : B → A) → f⁻¹ ∘ f ≡ id × f ∘ f⁻¹ ≡ id iso : ∀ {A} → A ≊ (⊤ → A) iso = const , flip _$_ tt , refl , refl

Cuando comenté la respuesta de Andrew (que por lo demás es muy buena), puede considerar los valores en un tipo como objetos de ese tipo como una categoría, y considerar las funciones como funtores. Para completar, aquí hay dos formas:

Establece como categorías aburridas

Una de las herramientas más utilizadas en matemáticas es un "setoide", es decir, un conjunto con una relación de equivalencia. Podemos pensar esto categóricamente a través del concepto de "grupo". Un groupoid es una categoría donde cada morfismo tiene una inversa tal que f . (inv f) = id f . (inv f) = id y (inv f) . f = id (inv f) . f = id .

¿Por qué esto captura la idea de una relación de equivalencia? Bueno, una relación de equivalencia debe ser reflexiva, pero esta es solo la afirmación categórica de que tiene flechas de identidad, y debe ser transitiva, pero esto es solo composición, finalmente tiene que ser simétrica (por eso agregamos inversas).

La noción ordinaria de igualdad en las matemáticas en cualquier conjunto da lugar a una estructura de grupo: ¡una en la que las únicas flechas son las flechas de identidad! Esto a menudo se llama la "categoría discreta".

Se deja como un ejercicio al lector para mostrar que todas las funciones son funcionadores entre categorías discretas.

Si tomas en serio esta idea, comienzas a preguntarte sobre los tipos con "igualdades" que no son solo identidad. Esto nos permitiría codificar "tipos de cocientes". Lo que es más, la estructura de grupo tiene algunos axiomas más (asociatividad, etc.) que son afirmaciones sobre "pruebas de igualdad de igualdad" que conducen por el camino de n-groupoids y la teoría de categoría superior. Esto es algo genial, aunque para ser útil necesitas tipos dependientes y algunos bits no totalmente resueltos, y cuando finalmente llegue a los lenguajes de programación debería permitir

data Rational where Frac :: Integer -> Integer -> Rational SameRationa :: (a*d) ~ (b*c) -> (Frac a b) ~ (Frac c d)

De tal forma que cada vez que modelaste, también tendrías que coincidir con el axioma de igualdad extra y así demostrar que tu función respetaba la relación de equivalencia en Rational Pero no te preocupes por esto. Lo único que resta es que la interpretación de la "categoría discreta" es una muy buena.

Enfoques Denotacionales

Cada tipo en Haskell está habitado por un valor extra, es decir undefined . ¿Qué está pasando con esto? Bueno, podríamos definir un orden parcial en cada tipo relacionado con cuán "definido" es un valor, tal que

forall a. undefined <= a

pero también cosas como

forall a a'' b b''. (a <= a'') // (b <= b'') -> ((a,b) <= (a'',b''))

Undefined está menos definido en que se refiere a un valor que no termina (en realidad, la función undefined se implementa lanzando una excepción en cada haskell, pero permite simular que undefined = undefined está undefined = undefined . No puede estar seguro de que algo no termine Si te dan un undefined todo lo que puedes hacer es esperar y ver. Por lo tanto, podría ser cualquier cosa.

Un orden parcial da lugar a una categoría de forma estándar.

Por lo tanto, cada tipo da lugar a una categoría donde los valores son objetos de esta manera.

¿Por qué son funciones functors? Bueno, una función no puede decir que se ha vuelto undefined debido al problema de detención. Como tal, tiene que devolver un undefined cuando encuentra uno, o tiene que producir la misma respuesta sin importar lo que se le haya dado. Te toca a ti demostrar que realmente es un funtor.