En Haskell, el functor de la clase de tipo Functor se define de la siguiente manera (véase, por ejemplo, la wiki de Haskell ):
class Functor (f :: * -> *) where
fmap :: (a -> b) -> f a -> f b
Por lo que yo entiendo (por favor, corríjanme si me equivoco), un funtor tal sólo puede tener como categoría objetivo una categoría construida utilizando un constructor de tipos, por ejemplo []
, Maybe
, etc. Por otro lado, uno puede pensar en palabras funcionales que tengan cualquiera de las categorías como objetivo de un functor, por ejemplo, la categoría de todos los tipos de Haskell. Por ejemplo, Int
podría ser un objeto en la categoría de destino de un functor, no solo Maybe Int
o [Int]
.
¿Cuál es la motivación de esta restricción en los funk de Haskell?
f
derecha? Y en su escenario,f
debe ser como una función normal de Haskell y asignar tipos a tipos. En Haskell, las únicas cosas que pueden tener el tipo* -> *
son los constructores de tipos. Las familias tipográficas son más generales, pero siempre deben aplicarse por completoRespuestas:
¡No hay restricción alguna! Cuando comencé a aprender la base teórica de categoría para los constructores de tipos, este mismo punto también me confundió. Llegaremos a eso. Pero primero, déjame aclarar algo de confusión. Estas dos citas:
y
Demuestre que está malinterpretando qué es un functor (o al menos, está haciendo un mal uso de la terminología).
Los functores no construyen categorías. Un functor es un mapeo entre categorías. Los functores traen objetos y morfismos (tipos y funciones) en la categoría de origen a objetos y morfismos en la categoría de destino.
Tenga en cuenta que esto significa que un functor es realmente un par de asignaciones: una asignación en objetos F_obj y una asignación en morfismos F_morph . En Haskell, la parte del objeto F_obj del functor es el nombre del constructor de tipos (p
List
. Ej. ), Mientras que la parte del morfismo es la funciónfmap
(depende del compilador de Haskell para resolver a quéfmap
nos referimos en cualquier expresión dada). Por lo tanto, no podemos decir queList
es un functor; solo la combinación deList
yfmap
es un functor. Aún así, las personas abusan de la notación; los programadores llaman aList
un functor, mientras que los teóricos de categoría usan el mismo símbolo para referirse a ambas partes del functor.Además, en la programación, casi todos los functores son endofunctores , es decir, la categoría de origen y la de destino son las mismas: la categoría de todos los tipos en nuestro idioma. Llamemos a esta categoría Tipo . Un endofunctor F en Tipo asigna un tipo T a otro tipo FT y una función T -> S a otra función FT -> FS . Este mapeo debe, por supuesto, obedecer las leyes de los functores.
Usando
List
como ejemplo: tenemos un constructor de tiposList : Type -> Type
y una funciónfmap: (a -> b) -> (List a -> List b)
, que juntos forman un functor. THay un último punto para aclarar. Escribir
List int
no crea un nuevo tipo de listas de enteros. Este tipo ya existía . Fue un objeto en nuestra categoría Tipo .List Int
es simplemente una forma de referirse a él.Ahora, se pregunta por qué un functor no puede asignar un tipo a, digamos,
Int
oString
. ¡Pero puede! Uno solo tiene que usar el functor de identidad. Para cualquier categoría C , el functor de identidad asigna cada objeto a sí mismo y el morfismo a sí mismo. Es sencillo verificar que este mapeo cumpla con las leyes de functor. En Haskell, este sería un constructor de tiposid : * -> *
que asigna cada tipo a sí mismo. Por ejemplo,id int
evalúa aint
.Además, incluso se pueden crear functores constantes , que asignan todos los tipos a un solo tipo. Por ejemplo, el functor
ToInt : * -> *
, dondeToInt a = int
para todos los tiposa
, y asigna todos los morfismos a la función de identidad entera:fmap f = \x -> x
fuente
f a
, dondef
es, hasta donde yo sé, un constructor de tipos. Por lo que recuerdo de la teoría de categorías, esto debe ser algún tipo de representación canónica (¿objeto inicial en una categoría de categorías? Tal vez estoy haciendo un mal uso de la terminología). De todos modos, leeré su respuesta cuidadosamente. Muchas gracias.[]
y:
. Quise decir esto por representación canónica.(_, int)
que toma un tipoa
al tipo de producto(a, int)
y una funciónf : 'a -> 'b
ag : 'a * int -> 'a * int
no es inductiva.f : 'a -> 'b
parag : 'a * int -> 'b * int
?"