¿Cómo son similares los funtores en Haskell y OCaml?

Desde un punto de vista práctico, se puede pensar en "funtores" en OCaml y Haskell como no relacionados. Como has dicho, en Haskell un funtor es cualquier tipo que te permite mapear una función sobre él. En OCaml, un funtor es un módulo parametrizado por otro módulo.

En Programación Funcional, ¿qué es un funtor?tiene una buena descripción de lo que son los funtores en las dos lenguas y cómo difieren .

Sin embargo, como su nombre lo indica, en realidad hay una conexión entre los dos conceptos aparentemente dispares! Los funtores de ambos lenguajes son solo realizaciones de un concepto de la teoría de categorías.

La teoría de categorías es el estudio de categorías, que son simplemente colecciones arbitrarias de objetos con "morfismos" entre ellos. La idea de una categoría es muy abstracta, por lo que "objetos" y "morfismos" pueden ser realmente cualquier cosa con algunas restricciones-tiene que haber un morfismo de identidad para cada objeto y los morfismos tienen que componer.

El más obvio ejemplo de una categoría es la categoría de conjuntos y funciones: los conjuntos son los objetos y las funciones entre conjuntos los morfismos. Claramente, cada conjunto tiene una función de identidad y las funciones se pueden componer. Una categoría muy similar se puede formar mirando un lenguaje de programación funcional como Haskell u OCaml: tipos concretos (por ejemplo, tipos con kind *) son los objetos y las funciones de Haskell/OCaml son los morfismos entre ellos.

En teoría de categorías, un funtor es un transformación entre categorías. Es como una función entre categorías. Cuando estamos mirando la categoría de tipos Haskell, un funtor es esencialmente una función de nivel de tipo: asigna tipos a otra cosa. El tipo particular de funtor que nos importa acerca de los tipos de mapas a otros tipos. Un ejemplo perfecto de esto es Maybe: Maybe mapas Int a Maybe Int, String a Maybe String y así sucesivamente. Proporciona una asignación para cada posible tipo Haskell.

Los funtores tienen un requisito adicional: tiene que mapear los morfismos de la categoría, así como los objetos. En particular, si tenemos un morfismos A → B y nuestra functor mapas A a A' y B a B', se tiene que asignar los morfismos A → B a algunos de morfismos A' → B'. Como ejemplo concreto, digamos que tenemos los tipos Int y String. Hay un montón de funciones de Haskell Int → String. Para que Maybe sea un funtor propio, tiene que tener una función Maybe Int → Maybe String para cada uno de ellos.

Felizmente, esto es exactamente lo que hace la función fmap: funciones de mapas. Para Maybe, tiene el tipo (a → b) → Maybe a → Maybe b; podemos agregar algunos paréntesis para obtener: (a → b) → (Maybe a → Maybe b). Lo que esta firma de tipo nos dice es que para cualquier función normal que tengamos, también tenemos una función correspondiente sobre Maybes.

Así que un funtor es una asignación entre tipos que también preserva las funciones entre ellos. La función fmap es esencialmente solo una prueba de esta segunda restricción sobre los funtores. Esto hace que sea fácil ver cómo la clase Haskell Functor es solo una versión particular de el concepto matemático.

Entonces, ¿qué pasa con OCaml? En OCaml, un funtor no es un tipo-es un módulo . En particular, es un módulo parametrizado: un módulo que toma otro módulo como argumento. Ya podemos ver algunos paralelismos: en Haskell, una Functor es como una función de nivel de tipo; en OCaml, un funtor es como una función de nivel de módulo . Así que en realidad, es la misma idea matemática; sin embargo, en lugar de ser utilizado en tipos -como en Haskell-se utiliza en módulos.

Hay muchos más detalles sobre cómo los funtores OCaml se relacionaron con la teoría de categorías en el sitio CS: ¿Cuál es la relación entre los funtores en SML y la teoría de categorías?. La pregunta habla de SML en lugar de OCaml per se, pero mi entendimiento es que el sistema de módulos de OCaml está muy estrechamente relacionado con el de SML.

En resumen: los funtores en Haskell y en OCaml son dos estructuras fundamentalmente diferentes que ocurren ser reificaciones de la misma idea matemática muy abstracta. Creo que es bastante limpio :).