2010-06-26 21 views

Respuesta

8

Un funtor contravariante de $ C $ a $ D $ es exactamente lo mismo que una normal (es decir, covariante) functor de $ C $ a $ D^{op} $, donde $ D^{op} $ es el opposite category de $ D $. Entonces, probablemente sea mejor entender primero las categorías opuestas, ¡entonces entenderás automáticamente los funtores contravariantes!

funtores contravariantes no vienen muy a menudo en el CS, aunque puedo pensar en dos excepciones:

  1. Es posible que haya oído hablar de contravarianza en el contexto de subtipos. Aunque técnicamente es el mismo término, la conexión es muy, muy débil. En la programación orientada a objetos, las clases forman un orden parcial; cada orden parcial es una categoría con "hom-sets binarios": dados dos objetos $ A $ y $ B $, hay exactamente un morfismo $ A \ a B $ iff $ A \ leq B $ (fíjese en la dirección; esta orientación ligeramente confusa es el estándar por razones que no explicaré aquí) y no tiene morfismos en caso contrario.

    Tipos parametrizados como, por ejemplo, Función parcial de Scala [-A, Unidad] son ​​funtores de esta categoría simple a sí mismo ... generalmente nos centramos en lo que hacen a los objetos: dada una clase X, Función parcial [X, Unidad] es también una clase. Pero los funtores preservan los morfismos también; en este caso si tuviéramos una subclase Dog of Animal, tendríamos un Morphism Dog $ \ to $ Animal, y el functor preservaría este morfismo, dándonos un morfismo PartialFunction [Animal, Unit] $ \ to $ PartialFunction [Dog, Unidad], diciéndonos que PartialFunction [Animal, Unit] es una subclase de PartialFunction [Dog, Unit]. Si piensas en eso, tiene sentido: supongamos que tienes una situación en la que necesitas una función que funcione en Perros. ¡Una función que funciona en todos los animales ciertamente funcionaría allí!

    Dicho esto, utilizar la teoría de categorías completa para hablar de conjuntos parcialmente ordenados es una gran exageración.

  2. Menos común, pero en realidad usa la teoría de categorías: considere la categoría Tipos (Hask) cuyos objetos son los tipos del lenguaje de programación Haskell y donde un morfismo $ \ tau_1 \ a \ tau_2 $ es una función del tipo $ \ tau_1 $ -> $ \ tau_2 $. También hay una categoría de Sentencias (Hask) cuyos objetos son listas de juicios de tipeo $ \ tau_1 \ vdash \ tau_2 $ y cuyos morfismos son pruebas de todos los juicios en una lista usando los juicios de la otra lista como hipótesis. Hay un funtor de los tipos (HASK) a los juicios (HASK) que tiene un Tipos (Hask) -morphism $ f: A \ a B $ a la prueba

 
    B |- Int 
    ---------- 
     ...... 
    ---------- 
    A |- Int 

que es un morfismo $ (B \ vdash Int) \ to (A \ vdash Int) $ - observe el cambio de dirección.Básicamente, lo que está diciendo es que si tienes una función que convierte a A en B'a, y una expresión de tipo Int con una variable libre x de tipo B, entonces puedes envolverlo con "let x = fy in. .. "y llegar a una expresión todavía de tipo Int pero cuya única variable libre es del tipo $ A $, no $ B $.

5
+0

Muy, muy agradable de hecho. Gracias por compartir. ¡Espero que salgan con 4 de N algún día! :) –

Cuestiones relacionadas