Siguiendo el mismo pensamiento que esta declaración de Andrej Bauer en esta respuesta
La comunidad de Haskell ha desarrollado una serie de técnicas inspiradas en la teoría de categorías, de las cuales las mónadas son más conocidas pero no deben confundirse con las mónadas .
¿Cuál es la relación entre los functores en SML y los functores en la teoría de categorías?
Como no conozco los detalles de los functores en otros idiomas, como Haskell u OCaml, si hay información de valor, agregue también secciones para otros idiomas.
Respuestas:
Las categorías forman una categoría (grande) cuyos objetos son las categorías (pequeñas) y cuyos morfismos son functores entre categorías pequeñas. En este sentido, los functores en la teoría de categorías son "morfismos de mayor tamaño".
Los functores de ML no son functors en el sentido categórico de la palabra. Pero son "funciones de mayor tamaño" en un sentido de tipo teórico.
Piense en tipos de datos concretos en un lenguaje de programación típico como "pequeños". Por lo tanto
int
,bool
,int -> int
, etc, son pequeños, las clases en Java son pequeñas, como así también estructuras en C. Podemos recopilar todos los tipos de datos en una gran colección llamadaType
. Un constructor de tipos, comolist
oarray
es una función deType
aType
. Por lo tanto, es una función "grande". Un functor de ML es solo una función grande un poco más complicada: acepta como argumento varias cosas pequeñas y devuelve varias cosas pequeñas. "Varias cosas pequeñas juntas" se conoce como estructura en ML. En términos de la teoría de tipos de Martin-Löf, tenemos un universoType
de tipos pequeños. Los tipos grandes generalmente se denominan tipos . Entonces tenemos:42 : int
)Type
(ejemplo:int : Type
)OrderedType
)list : Type -> Type
)String : OrderedType
)Map.Make : Map.OrderedType -> Make.S
)Ahora podemos trazar una analogía entre ML y categorías, según la cual los functores corresponden a los functores. Pero también notamos que los tipos de datos en ML son como "categorías pequeñas sin morfismos", en otras palabras, son como conjuntos más que como categorías. Podríamos usar una analogía entre ML y teoría de conjuntos:
fuente
Una estructura ML estándar es similar a un álgebra . Su firma describe una clase completa de álgebras de forma similar.
La mayoría de estas ideas fueron elaboradas en una serie de documentos por Burstall y Goguen al diseñar un lenguaje de especificación llamado CLEAR (Referencias c5 y c6 en la página DBLP ). David MacQueen estaba trabajando conjuntamente con Burstall y Sannella en ese momento, y estaba íntimamente familiarizado con los problemas El sistema de módulo ML estándar se basa en estas ideas.
Lo que la mayoría de la gente se pregunta es, ¿qué pasa con los morfismos? Los functores teóricos de categoría tienen una parte de objeto y una parte de morfismo. ¿Los functores ML estándar tienen lo mismo? La respuesta es sí y no.
¿Significa esto que ML estándar se está desviando de la teoría de categorías? No lo creo. Prefiero pensar que Standard ML está haciendo lo correcto, y la teoría de categorías aún no se ha puesto al día. La teoría de categorías aún no sabe cómo lidiar con las funciones de orden superior. Algún día lo hará.
fuente
Según mi conocimiento, no existe una relación formal entre los functores en la teoría de categorías y los functores en ML (SML u OCaml, están lo suficientemente cerca para nuestro propósito aquí).
En la teoría de categorías, los functores son funciones que operan en objetos. Están un nivel por encima de los morfismos, que a menudo son funciones que operan en elementos (muchas categorías tienen objetos que son conjuntos con alguna estructura algebraica y flechas que son homomorfismos entre estas estructuras). Un functor de ML es una función que opera en módulos, un nivel por encima de las funciones que operan en valores del lenguaje central. Creo que el parecido se detiene aquí.
Los functores de ML fueron bautizados por Dave McQueen en su revisión de 1985 de Módulos para ML estándar (citeseerx) que apareció en el Boletín de Polimorfismo (el documento original usó la expresión "módulo paramétrico"; las publicaciones posteriores tienden a usar el adjetivo "parametrizado"). Lamentablemente, no puedo encontrar una copia de ese documento. En su artículo de 1986 Usando tipos dependientes para expresar estructura modular (citeseerx) , da el nombre establecido.
fuente