haskell - superarla - dependencia emocional pdf

Tipos dependientes: ¿cómo es el tipo de pareja dependiente análoga a una unión disjunta? (6)

He estado estudiando tipos dependientes y entiendo lo siguiente:

Por qué la cuantificación universal se representa como un tipo de función dependiente. ∀(x:A).B(x) significa "para todas las x del tipo A hay un valor de tipo B(x) " . Por lo tanto, se representa como una función que, cuando se le da cualquier valor x de tipo A devuelve un valor de tipo B(x) .
¿Por qué la cuantificación existencial se representa como un tipo de par dependiente? ∃(x:A).B(x) significa "existe una x de tipo A para la cual hay un valor de tipo B(x) " . Por lo tanto, se representa como un par cuyo primer elemento es un valor particular x de tipo A y cuyo segundo elemento es un valor de tipo B(x) .

Aparte: también es interesante observar que la cuantificación universal siempre se usa con la implicación material, mientras que la cuantificación existencial siempre se usa con la conjunción lógica .

De todos modos, el artículo de Wikipedia sobre tipos dependientes establece que:

Lo opuesto al tipo dependiente es el tipo de par dependiente , tipo de suma dependiente o tipo sigma . Es análogo al coproducto o unión disjunta.

¿Cómo es que un tipo de pareja (que normalmente es un tipo de producto) es análogo a una unión disjunta (que es un tipo de suma)? Esto siempre me ha confundido.

Además, ¿cómo es el tipo de función dependiente análoga al tipo de producto?

Basándose en la respuesta de Petr Pudlák, otro ángulo para ver esto de una manera puramente no dependiente es notar que el tipo Either aa es isomorfo al tipo (Bool, a) . Aunque este último es, a primera vista, un producto, tiene sentido decir que es un tipo de suma, ya que es la suma de dos instancias de a .

Tengo que hacer este ejemplo con Either aa lugar de Either ab , porque para que este último se exprese como un producto, necesitamos tipos bien dependientes.

Buena pregunta. El nombre podría provenir de Martin-Löf, que utilizó el término "producto cartesiano de una familia de conjuntos" para el tipo pi. Vea las siguientes notas, por ejemplo: http://www.cs.cmu.edu/afs/cs/Web/People/crary/819-f09/Martin-Lof80.pdf El punto es que mientras que un tipo pi es en principio parecido a una exponencial, siempre se puede ver una exponencial como un producto n-ary donde n es el exponente. Más concretamente, la función no dependiente A -> B se puede ver como un tipo exponencial B ^ A o un producto infinito Pi_ {a en A} B = B x B x B x ... x B (A veces). Un producto dependiente es en este sentido un producto potencialmente infinito Pi_ {a en A} B (a) = B (a_1) x B (a_2) x ... x B (a_n) (una vez por cada a_i en A).

El razonamiento para la suma dependiente podría ser similar, ya que puede ver un producto como una suma n-aria donde n es uno de los factores del producto.

Esto probablemente sea redundante con las otras respuestas en este punto, pero aquí está el núcleo del problema:

¿Cómo es que un tipo de pareja (que normalmente es un tipo de producto) es análogo a una unión disjunta (que es un tipo de suma)? Esto siempre me ha confundido.

Pero, ¿qué es un producto sino una suma de números iguales? por ejemplo, 4 × 3 = 3 + 3 + 3 + 3.

La misma relación vale para tipos, conjuntos o cosas similares. De hecho, los enteros no negativos son solo la decategorización de conjuntos finitos. Las definiciones de suma y multiplicación en números se eligen de modo que la cardinalidad de una unión disjunta de conjuntos es la suma de las cardinalidades de los conjuntos, y la cardinalidad de un producto de conjuntos es igual al producto de las cardinalidades de los conjuntos. De hecho, si sustituyes "establecer" por "rebaño de ovejas", esta es probablemente la forma en que se inventó la aritmética.

La confusión surge del uso de terminología similar para la estructura de un tipo and y de cómo se ven sus valores.

Un valor de Σ (x: A) B (x) es un par (a, b) donde a∈A y b∈B (a) . El tipo del segundo elemento depende del valor del primero.

Si observamos la estructura de Σ (x: A) B (x) , es una unión disjunta (coproducto) de B (x) para todos los posibles x∈A .

Si B (x) es constante (independiente de x ) entonces Σ (x: A) B será solo | A | copias de B , que es A⨯B (un producto de 2 tipos).

Si miramos la estructura de Π (x: A) B (x) , es un producto de B (x) para todos los posibles x∈A . Sus valores se pueden ver como | A | -tuples donde un -th componente es de tipo B (a) .

Si B (x) es constante (independiente de x ) entonces Π (x: A) B será simplemente A → B - funciones de A a B , es decir Bᴬ ( B a A ) usando la notación de la teoría de conjuntos - el producto de | A | copias de B.

Entonces Σ (x∈A) B (x) es un | A | -ary coproducto indexado por los elementos de A , mientras que Π (x∈A) B (x) es un | A | -ary producto indexado por los elementos de A.

Primero, vea qué es un coproducto.

Un coproducto es un objeto terminal A para todos los objetos B_i de modo que para todas las flechas B_i -> X hay una flecha B_i -> A, y una única A -> X tal que los triángulos correspondientes conmutan.

Puede ver esto como un tipo de datos Haskell A con B_i -> A siendo un grupo de constructores con un único argumento de tipo B_i. Está claro, entonces, que por cada B_i -> X es posible suministrar una flecha desde A -> X, de modo que a través de la coincidencia de patrones, podrías aplicar esa flecha a B_i para obtener X.

La conexión importante con los tipos sigma es que el índice i en B_i puede ser de cualquier tipo, no solo un tipo de números naturales.

La diferencia importante de las respuestas anteriores es que no tiene que tener un B_i para cada valor i de ese tipo: una vez que ha definido B_i ∀ i, tiene una función total.

La diferencia entre Π y Σ, como se puede ver en la respuesta de Petr Pudlak, es que para Σ algunos de los valores B_i en la tupla pueden estar ausentes - para algunos i puede que no haya B_i correspondiente.

La otra diferencia clara entre Π y Σ es que Π caracteriza a un producto de B_i al proporcionar i-ésima proyección del producto Π a cada B_i (esto es lo que significa la función i -> B_i), pero Σ proporciona las flechas hacia el otro lado alrededor - proporciona la inyección i-th de B_i en Σ.

Un par dependiente se escribe con un tipo y una función de valores de ese tipo a otro tipo. El par dependiente tiene valores de pares de un valor del primer tipo y un valor del segundo tipo aplicado al primer valor.

data Sg (S : Set) (T : S -> Set) : Set where Ex : (s : S) -> T s -> Sg S T

Podemos recapturar tipos de suma mostrando cómo Either se expresa canónicamente como un tipo sigma: es simplemente Sg Bool (choice ab) donde

choice : a -> a -> Bool -> a choice l r True = l choice l r False = r

es el eliminador canónico de booleanos.

eitherIsSg : {a b : Set} -> Either a b -> Sg Bool (choice a b) eitherIsSg (Left a) = Sg True a eitherIsSg (Right b) = Sg False b sgIsEither : {a b : Set} -> Sg Bool (choice a b) -> Either a b sgIsEither (Sg True a) = Left a sgIsEither (Sg False b) = Right b