Mostrando entradas con la etiqueta variancia. Mostrar todas las entradas
Mostrando entradas con la etiqueta variancia. Mostrar todas las entradas

domingo, 19 de mayo de 2013

Álgebras y coálgebras

He encontrado varias veces por Internet la pregunta de qué es un coálgebra y las respuestas han sido más o menos liosas. El motivo es que en computación al hablar de (co)álgebras nos referimos a las F-(co)álgebras. Lo que implica explicar qué es la F y esa F es un funtor. Un funtor es una operación en categorías y hay que introducir parte de la teoría de categorías para explicarlo.

Puede hacerse más simple.

El producto cartesiano generalizado

Estrictamente hablando el producto cartesiano es una operación entre dos conjuntos.[$$A\times B$$]El resultado es otro conjunto y sus elementos son los pares ordenados de forma que el primer elemento se obtenga del primer conjunto y el segundo elemento del segundo. En notación matemática:[$$A\times B = \{ (a,b) \mid a\in A, b\in B \}$$] Cuando hacemos dos productos cartesianos, surge la duda de si es asociativo o no.[$$A\times (B \times C) \overset{?}{=} (A\times B)\times C$$] En general el producto cartesiano no es asociativo, ya que [$(a,(b,c))\ne((a,b),c)$], pero nada impide usar un producto cartesiano generalizado (que escribiré entre paréntesis) en el cual el producto de tres conjuntos no sean pares, sino triplas. [$$(A\times B \times C) = \{ (a,b,c) \mid a\in A, b\in B, c\in C \}$$] El de cuatro conjuntos serían cuadruplas y el de [$n$] conjuntos lo que llamaremos [$n$]-tuplas. [$$(A_1\times\cdots\times A_n) = \{(a_1,\dots,a_n) \mid a_1\in A_1,\dots,a_n\in A_n \}$$] Usaremos este producto cartesiano generalizado.

Antes de acabar este apartado sólo resta destacar un caso particular. El del producto cartesiano de cero conjuntos. Llamaremos a este conjunto [$1$] y sólo contiene un elemento que es la tupla vacía [$()$].

Esta definición no debe ser extraña si seguimos la siguiente secuencia. [$$(A\times B \times C) = \{ (a,b,c) \mid a\in A, b\in B, c\in C \}$$][$$(A\times B) = \{ (a,b) \mid a\in A, b\in B \}$$][$$(A) = \{ (a) \mid a\in A \}$$][$$1 = \{ () \}$$]

Algebras

La idea de usar álgebras proviene de tomar un tipo de datos como sus valores y las operaciones que los construyen por inducción. Por ejemplo, en el caso de una lista, estos constructores serían.
  • La lista vacía. Lo que se ha venido a llamar la constante nil.
  • Añadir un elemento a la lista. Función que se llama cons.
Las constantes se expresan como funciones que no toman argumentos (mejor dicho, toman la tupla vacía), por lo que si la lista es de enteros y llamo al tipo de esta lista [int], el tipo de cada una de estas funciones sería: [$$nil : 1 \to [int]$$]Que no toma argumentos y devuelve la lista de enteros vacía y[$$cons : (int \times [int]) \to [int]$$]Que toma un entero y una lista de enteros y devuelve otra con este elemento añadido.

Teniendo en mente estas funciones, decimos que el tipo lista de enteros [int] no es más que el conjunto de sus valores (que llamaré [$A_{[int]}$]) y las dos funciones que los construyen por inducción. [$$(A_{[int]}, nil : 1\to[int] , cons : (int \times [int]) \to [int] )$$]Muy similar a, por ejemplo, un monoide [$$(M,e:1 \to M ,\otimes:(M\times M)\to M )$$] donde [$M$] son los elementos del monoide, [$e$] el elemento neutro y [$\otimes$] la operación interna. O a la definición de los números naturales[$$(N,cero:1\to N, suc:N \to N)$$] donde [$cero$] es la constante cero y [$suc$] la operación que obtiene el siguiente número natural (el sucesor).

Generalizando de nuevo, vemos que todas estas definiciones tienen siempre la misma estructura.[$$(A, f_1: X_1 \to A,\dots, f_n: X_n \to A)$$]Donde los [$X_i$] son productos cartesianos de conjuntos en los cuales puede estar el propio [$A$] o no.

Bien. Eso es un álgebra. Un conjunto y varias operaciones cuyo codominio es tal conjunto.

Coálgebras

En un coálgebra lo que tenemos es [$$(A, f_1: A\to X_1,\dots, f_n: A\to X_n)$$] En este caso las operaciones tienen el conjunto en su dominio.

¿Qué significado tiene esto?

Pensemos en una lista. La operación cons tomaba una lista y un elemento e introducía ese elemento en la lista.

cons(7,[1,2,3])=[7,1,2,3]
cons(9,[8,1,3])=[9,8,1,3]
cons(4,[])=[4]

El tipo de cons era [$(int\times [int])\to [int]$]. En una coálgebra la operación correspondiente (que llamaremos headtail) deberá tener el tipo [$[int]\to(int\times [int])$] lo que significa que de una lista obtenemos un elemento y otra lista. Una forma de ver esto es pensar que, en la coálgebra, la operación headtail extrae un elemento de la lista. En general, las operaciones de una coálgebra deshacen lo que los constructores hacían en las álgebras. Por esta razón a las operaciones de una coálgebra se las denomina destructores.

headtail([1,2,3])=(1,[2,3])
headtail ([8,1,3])=(8,[1,3])
headtail ([])=????

¿Qué pasó en este último ejemplo? ¿Es realmente headtail una función sobre las listas o sólo sobre las listas no vacías?

Existen dos respuestas aquí.

La primera respuesta es introducir los tipos suma. De esa manera, headtail podría devolver un error sumando el conjunto unidad al tipo de su codominio ([$headtail: [int]\to 1+(int\times [int])$]). Esto es dual a la agrupación de todas las operaciones del álgebra de la lista en una única operación sumando sus dominios ([$nilcons: 1+(int\times [int])\to [int]$]) y por esta vía definimos el funtor polinómico [$F X = 1+(X\times [X])$] y llegamos a las F-(co)álgebras que es de lo que realmente estamos hablando.

Aún introduciendo la posibilidad de que headtail acabe de leer una lista, no significa que lo haga. Usar coinducción permite trabajar con listas infinitas en las cuales siempre podemos ir extrayendo elementos. Esto nos lleva a...

La segunda respuesta es modificar nuestro tipo de datos y decir que no trabajamos con listas, sino con listas infinitas (los llamados streams). Como la lista es infinita, nunca va a estar vacía y siempre podremos usar headtail. Estos tipos de datos infinitos definidos por coálgebras y coinducción se denominan codatos. Son útiles para modelar, por ejemplo, la entrada del usuario que, en principio, nunca acaba.

jueves, 20 de mayo de 2010

Tipos intersección

¿Qué son?

Supongamos que tenemos una función con el siguiente tipo

[$$ f: A \rightarrow B \rightarrow C $$]

¿Cuál es el tipo de esta nueva función?

[$$ \lambda x. f x x $$]

Esta claro que la x tendrá que ser de tipo A y de tipo B. Si tuviéramos subtipos, y asumiendo que el tipo de x es X, diríamos

[$$ X\le A,\quad X\le B $$]

Sería tarea del motor de inferencia buscar el tipo adecuado. Por otra parte, podríamos introducir una solución tramposa. Inventarnos el tipo

[$$ X=A\cap B $$]

con las  propiedades

[$$ T\cap S \le T $$]
[$$
T\cap S \le S $$]

Ni que decir tiene que esto recuerda mucho al concepto de intersección de conjuntos, de ahí el nombre.

El sistema de Coppo-Dezani

Si introducimos las reglas usuales de una intersección (es decir, las de un ínfimo) obtenemos el sistema de Coppo-Dezani (sistema CD). Este sistema tiene unas cualidades muy interesantes.

  • Cumple la reducción de sujeto. Es lo mínimo que se puede pedir a un sistema de tipos para una estrategia de evaluación por nombre: que si evaluamos en un paso nuestra expresión (sea el redex que sea), el tipo siga siendo el mismo.
  • Los términos tipables son los términos fuertemente normalizables. O sea, que sólo podremos darle un tipo a los términos cuya evaluación acabe.
  • Las formas normales son tipables ya que no tienen más pasos de evaluación.
  • Cumple la expansión de sujeto. Esto es interesante. Si damos un paso de evaluación marcha atrás, el tipo también se mantiene.
  • Estas propiedades nos llevan a la gran característica definitoria del sistema CD: Un término es tipable si y sólo si su evaluación acaba sea cual sea la estrategia de evaluación (es fuertemente normalizable).

Esta última propiedad no es buena. Y no lo es porque significa que no podemos darle un tipo a expresiones de la forma

[$$ K x y = x $$]
[$$ K\; 3\;((\lambda z. z z)(\lambda z. z z)) $$]

La función K (el combinador K) descarta su segundo parámetro, por lo que el término debería tener tipo entero (el resultado es 3). Sin embargo, no es tipable porque el segundo argumento nunca termina su evaluación. Este término no es fuertemente normalizable, es sólo normalizable de cabeza.

El sistema de Coppo-Dezani-Venneri

La solución es añadir una constante ? que significa "cualquier cosa". Sería vista como la intersección nula o como el elemento neutro de la intersección.

[$$ \omega \cap X = X $$]
[$$ X \cap \omega = X $$]

Al añadir las reglas apropiadas para introducir esta constante, los autores del sistema CDV se vieron forzados a separar los tipos en dos niveles. El nivel de tipo simple y el nivel de intersección (o secuencia) de tipos.

[$$ \tau ::= X\;\mid\;\omega\;\mid\;\sigma \rightarrow \tau $$]
[$$ \sigma ::= \tau_1 \cap \cdots \cap \tau_n\qquad (n>0) $$]

Con este sistema, las propiedad principal es que se puede asignar un tipo a los términos con forma normal de cabeza.

El sistema de Barendregt-Coppo-Dezani

El problema de los tipos restringidos del sistema CDV se soluciona introduciendo una relación de subtipo. Esto es así porque en posición covariante las intersecciones distribuyen.

[$$ A\rightarrow (B\cap C)=(A\rightarrow B)\cap(A\rightarrow C) $$]

Introduciendo una relación de subtipo que sea un preorden se puede derivar una clase de equivalencia y trabajar con el orden parcial generado en el conjunto cociente.

Este sistema es bastante más complejo. La relación de subtipo tiene hasta ocho reglas. La relación de tipado tiene seis reglas.

El sistema BCD tiene la misma potencia que el CDV. Sin embargo tiene un gran fallo: existen varias formas de demostrar que una expresión tiene un tipo. Las reglas no son dirigidas sintácticamente.

A pesar de todo esto, el sistema BCD es el más conocido y usado de los sistemas de tipos intersección.

miércoles, 14 de octubre de 2009

Covariancia y contravariancia (V)

Funciones virtuales

En el último post de esta serie dije que la siguiente operación no se podía realizar.

pes.crea_mueble(150) // Mal, no sabemos las patas que tiene la silla

Esto puede soslayarse si el programador asume la responsabilidad de actualizar correctamente el estado de la silla entera cuando se modifica únicamente la parte mueble de la misma. Por ejemplo, en el caso anterior el programador puede usar una versión especial de crea_mueble() para las sillas. En esta versión especial puede optar por, por ejemplo, usar cuatro patas por defecto.

Ahora bien, ¿cómo sabe que, aunque sea un puntero a mueble, realmente es una silla? Se usa lo que se llaman funciones virtuales. Una función virtual es aquella cuyo despacho se realiza en función del tipo de objeto apuntado y no en función del tipo de puntero. De esta forma, aunque tengamos un puntero a mueble, si actuamos sobre una silla, se usará la función especial de la silla.

Con esta técnica, y bajo responsabilidad del programador, los punteros de lectura/escritura terminan siendo como los punteros de lectura: covariantes.

Paso por valor

En otro post dije que la herencia no era lo mismo que el subtipado y di un motivo en concreto: el tamaño que ocupan los objetos en memoria. Si usamos punteros (o referencias) a objetos podemos usar la técnica de arriba, pero si nuestro lenguaje es de paso por valor, tenemos un problema.

Supongamos que una función tiene el tipo f: Unit -> A. Esta función no toma ningún argumento (el tipo unit es algo así como el tipo void en C/C++ en este caso) y devuelve un objeto de tipo A. Claro está que podría devolver un subtipo B de A.

Por lo mencionado antes, los lenguajes orientados a objetos no usan realmente la relación de subtipo. Usan la relación de herencia. Eso significa que B puede ser de mayor tamaño que A y aquí surge el problema: ¿cómo sabe la función llamante si f va a devolver un A o algún otro tipo heredado como B? Porque si va a devolver un B va a tener que reservar más memoria que para un A. En caso contrario tendríamos un desbordamiento de buffer (buffer overflow).

Una solución sería pensar que la función tiene que devolver exactamente un A. Esto la haría invariante y que no podríamos cambiar cualquier aparición de f: Unit -> A por otra función g: Unit -> B.

Por otra parte, sabemos que con los punteros (y gracias a las funciones virtuales) no tenemos ese problema. Es decir, que sí podemos cambiar cualquier aparición de f2: Unit -> PA por otra función g2: Unit -> PB.

¡Pero es que es lógico! Pasamos los punteros por valor y el objeto apuntado por referencia. Los punteros son todos del mismo tamaño por lo que no hay problemas de desbordamiento de buffer. Esto es justo lo que hace el C++: permitir la covariancia de funciones sólo para los punteros (y referencias).

Marcando la variancia en los constructores de tipo

La solución de C++ está bastante encorsetada. Sólo permite covariancia para unos tipos predefindos. ¿No podríamos mejorar esto?

Si el programador supiese que, cuando usa un constructor de tipos, el resultado es otro tipo que

  1. Va a tener estados consistentes y no va a tener slicing (funciones virtuales)
  2. No va a provocar desbordamiento de buffer (mismo tamaño si es paso por valor)
  3. No va a tener problemas semánticos (el programador es responsable y sabe lo que se hace).

Entonces podría asegurar que sus constructores de tipos van a ser covariantes o contravariantes y podría anotarlo en el código. Por ejemplo, un contenedor de sólo lectura es covariante.

Esto es lo que hace el lenguaje de programación Scala y las nuevas versiones del C#. Un ejemplo obtenido de aquí es:

//+A significa que es covariante en A

class Stack[+A] { 

//B >: A significa que A es subtipo de B (A<:B)

def push[B >: A](elem: B): Stack[B] = new Stack[B] {
override def top: B = elem
override def pop: Stack[B] = Stack.this
override def toString() = elem.toString() + " " +
Stack.this.toString()
}

def top: A = error("no element on stack")

def pop: Stack[A] = error("no element on stack")

override def toString() = ""
}

object VariancesTest extends Application {

var s: Stack[Any] = new Stack().push("hello");
s = s.push(new Object())
s = s.push(7)
Console.println(s)

}

Comentarios finales

Con esto doy por acabada la serie de variancias. Seguramente surgirá algún tema más que comentar en el futuro, por lo que no tendré ninguna pereza en reabrirla para nuevos posts. 

martes, 1 de septiembre de 2009

Covariancia y contravariancia (IV)

El problema de los punteros

Supongamos que tenemos tres tipos de punteros. Los punteros de sólo lectura, los de sólo escritura y los de escritura-lectura. Si apuntan a un tipo T, los llamaremos respectivamente PL(T), PE(T) y P(T).

Debe estar claro que si un puntero es de escritura-lectura entonces es de escritura y de lectura.

PL(T) <: P(T)

PE(T) <: P(T)

Ahora bien, lo que no está tan claro es si tengo un tipo y un subtipo (como los muebles M y las sillas S) si ocurrirá que

PL(S) <: PL(M) ???

PE(S) <: PE(M) ???

P(S) <: P(M) ???

PL(S) <: P(M) ???

Y todas las dieciocho combinaciones.

Para dilucidar si los punteros son covariantes o contravariantes vamos a inventarnos unas operaciones de lectura y de escritura sobre ellos. Estas operaciones serán:

  • altura(): Devuelve la altura de un mueble.
  • patas(): Devuelve el número de patas de un mueble.
  • crea_silla(int, int): Crea una silla con la altura y el número de patas dados
  • crea_mueble(int): Crea un mueble con la altura dada.

Ahora, usaremos los punteros plm de tipo PL(M), pls de tipo PL(S), pem de tipo PE(M) y pes de tipo PE(S) y veremos cuándo se pueden o no sustituir unos por otros.

pls.patas() //OK, mismo tipo

plm.patas() //Mal, los muebles no tienen patas

plm.altura() // OK, mismo tipo

pls.altura() //Bien, las sillas tienen altura

pes.crea_silla(110, 4) // OK, mismo tipo

pem.crea_silla(110, 4) // Bien, creamos un mueble que es una silla

pem.crea_mueble(150) // OK, mismo tipo

pes.crea_mueble(150) // Mal, no sabemos las patas que tiene la silla

En definitiva, hemos podido usar PL(S) donde había un PL(M) y hemos podido usar un PE(M) donde había un PE(S) de forma que:

S <: M

PL(S) <: PL(M)

PE(S) :> PE(M)

Los punteros de lectura son covariantes y los de escritura son contravariantes. Obviamente, como los punteros de escritura-lectura tienen que compartir ambas propiedades, llegamos a la conclusión que o bien S=M o bien no hay forma de relacionar P(S) con P(M). Esto se puede ver en el libro de Pierce, en el apartado 15.5.

La conversión de const char** a char** 

Este curioso comportamiento tiene sus repercusiones en lenguajes como el C++ y particularmente en las conversionse de cualificación CV. En estas conversiones se prohibe la conversión de "un puntero a un puntero a un dato constante" a "un puntero a un puntero a un dato modificable". ¿Por qué? Veamos los tipos:

const char**  char**

P(PL(T))      P(P(T))

Como el constructor de tipos más exterior es el puntero de escritura-lectura, no podemos decir nada de su relación con el otro puntero.

Esto suele extrañar a la gente porque si sólo fueran punteros de un nivel tendríamos

const char*    char*

PL(T)       <: P(T)

Y la conversión sería posible. Cualquier programador de C++ sabe que podemos pasar un puntero normal donde se requiere un puntero constante.

En la siguiente parte veremos la relación del slicing con los punteros de escritura, cómo usar el conocimiento sobre la variancia en los constructores de tipo y la forma que tienen algunos lenguajes de trabajar con la variancia de tipos.

lunes, 24 de agosto de 2009

Covariancia y contravariancia (III)

Regla general

Estamos llegando a una regla más o menos universal que es: lo que se escribe desde fuera del tipo se hace contravariante, lo que se lee desde fuera del tipo se hace covariante.

En una función: Se pasan (escriben) argumentos y se devuelve (lee) el retorno. Las funciones son contravariantes en los argumentos y covariantes en el retorno.

Esto tiene que matizarse y veremos por qué en el siguiente apartado.

Menos por menos es más

Ahora vamos a hacer un esfuerzo mental para pensar en lo que ocurre cuando pasamos una función a otra función.

La función "total_sillas" tiene el siguiente tipo:

total_sillas ::  (S -> int) -> int

Esta función conoce de alguna manera todas las sillas de mi casa y usa la función que se le pasa de argumento (la S -> int) para obtener alguna propiedad numérica de estas sillas. Finalmente, retorna la suma total de estos números.

La función "total_muebles" es igual, pero trabaja con los muebles.

total_muebles :: (M -> int) -> int

Como propiedades numéricas vamos a usar estas dos funciones:

cuenta_patas :: S -> int

altura_mueble :: M -> int

Ahora vamos a ver si una se puede usar donde la otra o no.

total_muebles(altura_mueble) // OK, mismo tipo

total_sillas(altura_muebles)//Bien,las sillas tienen altura

total_sillas(cuenta_patas) //OK, mismo tipo

total_muebles(cuenta_patas) //Mal, hay muebles sin patas

Así que puedo usar "total_sillas" donde usaba "total_muebles", es decir:

 S                 <:   M

(S -> int) -> int  <:  (M -> int) -> int

Lo que significa que ¡es covariante! Esto es muy curioso porque los argumentos de una función eran contravariantes, pero los argumentos de los argumentos que serían contra-contravariantes son covariantes.

La moraleja a recordar es: La contravariancia es como el menos en la multiplicación, menos por menos es más. O sea, contravariante de contravariante es covariante.

Esto nos lleva a una regla muy usada en la teoría de tipos que es: Será covariante si está a la izquierda de un número par de "->" y contravariante en caso contrario. Esta regla se puede ver en el capítulo dedicado a la teoría de tipos del manual de las ciencias de la computación escrito por Cardelli. En la página 28.

Escribiré "cov" cuando sea covariante y "con" cuando sea contravariante en estos ejemplos:

con ->  con -> cov   (Se asocia por la derecha)

(cov -> con) -> cov

con-> (cov -> con) -> cov

(cov -> cov -> con) -> cov

((con -> cov) -> con) ->cov

En la siguiente parte de este serial veremos cómo afecta la mutabilidad a la variancia de tipos mediante el uso de punteros.

Covariancia y contravariancia (II)

Las listas y otros contenedores

Las transformaciones de tipos más simples, y las que veremos aquí, son las de construcción de nuevos tipos. Vamos a empezar por un constructor de tipos simple. Pasar de un tipo T a una lista de este tipo L(T).

Entonces, una lista de muebles lm de es de tipo L(M) y una lista de sillas ls de tipo L(S). ¿Puedo usar una donde la otra? ¿Y al revés?

Está claro que puedo usar una lista de sillas cuando me pidan una lista de muebles, pero no al revés. Así que:

S    <: M
L(S) <: L(M)

Llegando a la conclusión de que esta transformación de tipos es covariante. En general esto pasa con todos los contenedores.

Los argumentos de las funciones

Las funciones son otros constructores de tipos. Si tengo un tipo T1 y otro tipo T2, el tipo de una función que toma un argumento T1 y devuelve un valor T2 será  T1 -> T2.

¿Son las funciones covariantes o contravariantes? Empezaremos por una función simple a ver qué ocurre.

fs :: S -> Int  //fs es una función que toma una silla y devuelve un Int
fm :: M -> int  //fm es una función que toma un mueble y devuelve un Int

Tengo las siguientes posibilidades:

fm(m) //OK: Mismo tipo
fs(m) //Uso fs donde usaba fm: Mal, requiero una silla y me dan un mueble
fs(s) //OK: Mismo tipo
fm(s) //Uso fm donde usaba fs: Bien, requiero un mueble y me dan una silla

Es decir, que puedo usar "fm" por "fs" pero no al revés.

S        <: M
S -> Int :> M -> int

Así que las funciones son contravariantes si nos fijamos en sus argumentos.

Los retornos de las funciones

Si hacemos lo propio con los retornos, ¿qué pasará?

fs :: Int -> S  //fs es una función que toma un Int y devuelve una silla
fm :: Int -> M  //fm es una función que toma un Int y devuelve un M
s=fs(1) //OK mismo tipo
s=fm(1) //Mal, no todos los muebles son sillas
m=fm(1) //OK mismo tipo
m=fs(1) //Bien, una silla es un mueble

Entonces

S        <: M
S -> Int <: M -> int

Así que las funciones son covariantes si nos fijamos en sus retornos.

Es importante destacar a partir de ahora que la variancia dependerá de en qué argumento del constructor de tipos nos fijamos. Así pues diremos que el constructor de funciones -> es contravariante en el tipo de su izquierda (el argumento) y covariante en el de la derecha (el retorno).

En la siguiente parte veremos qué ocurre si usamos funciones que tomen o devuelvan funciones. Lo que se denominan funciones de alto nivel.

Covariancia y contravariancia (I)

Covariancia y contravariancia en el álgebra lineal.
En el álgebra lineal el concepto de variancia tiene que ver con el tipo de transformación que realiza una cantidad bajo un cambio de base. Si la transformación es con la base será covariante, si es en contra de la base será contravariante.
Por ejemplo, si mi base es
[$$B=\left\{e_1,e_2\right\}$$]
y tengo un vector
[$$V=3 e_1 + 4 e_2$$]
Si cambio la base a
[$$B'=\left\{e'_1,e'_2\right\}=\left\{2e_1,4e_2\right\}$$]
Para que el vector siga siendo el mismo los componentes tienen que cambiar. Ahora
[$$V=\frac{3}{2}e'_1 + e'_2$$]
Los componentes son contravariantes porque compensan el cambio de base. Por ejemplo, el primer vector de la base creció al doble mientras que ese mismo componente se redujo a la mitad.
La base en sí es covariante aunque esto sea trivial.
Es importante aquí resaltar que un objeto matemático que se transforme de manera contraria a uno contravariante debe ser covariante. En ese sentido la contravariancia es como el menos en la multiplicación. Menos por menos es más. Contravariante de contravariante es covariante.
Covariancia y contravariancia en la teoría de tipos.
Aunque en la teoría de tipos la cosa es bastante distinta, ambos tipos de variancia provienen de la correspondiente variancia en las categorías. No voy a seguir por aquí. Quién quiera saber más debería leer este libro de Pierce.
Centrándonos en la teoría de tipos, la covariancia y contravariancia tiene que ver con la relación de herencia de los tipos. Si el tipo S (las sillas) es un refinamiento del tipo M (muebles) diremos que
[$$S <: M$$]
Esto es más o menos obvio. El tipo de las sillas es un refinamiento del tipo de los muebles. El tipo de las sillas es menor que el tipo de los muebles.
Si tengo una transformación de tipos T y el resultado es que
[$$T(S) <: T(M)$$]
Entonces la transformación es covariante. Sin embargo, si la transformación es
[$$T(S) :> T(M)$$]
diremos que es contravariante.
¿Para qué sirve esto? La respuesta en el siguiente post dedicado al tema.