He recogido el Homotopy Tipo de libro de la Teoría para el ocio. Me siento cómodo con establecimiento inflexible de tipos de idiomas y familiar con dependencia escrito de los idiomas y me gusta la topología, por lo que pensé que la HoTT libro fue una buena oportunidad para aprender algunas de las matemáticas subyacentes a los sistemas de tipo (y, por HoTT la reputación de una nueva manera de mirar muchas otras cosas que yo sé.)
Yo había incursionado un poco en el sector formal del tipo de la teoría anterior a HoTT. Durante mucho tiempo he pensado (independiente), tipos como este:
Unidad de tipos de datos son tipos con un único valor, isomorfo a:
data Unity = Unity
Se puede resumir los tipos, la creación de un tipo habitada por tantos valores como A + B
data Sum a b = Left a | Right b
más comúnmente conocido como Either a b en la programación de los círculos.
Luego están los tipos de productos, que la casa de tantos tipos como A × B
data Product a b = Both a b
más comúnmente conocido como (a, b).
Por último, hay exponencial tipos habitada por tantos valores como hay asignaciones A → B (que es $B^A$). Estos son más comúnmente conocidos como funciones, y la definición de ellos es mi día de trabajo. El poco algebraicas del tipo de teoría que sé que está fundado en esos supuestos. (Tengo curiosidad por lo que está más allá exponencial tipos en esta progresión, sino que es además el punto).
La HoTT libro comienza por definir la exponencial de tipo $\rightarrow$, el dependiente de la función de tipo de $\Pi$, el tipo de producto $\times$, y el dependiente de par tipo de $\Sigma$. Las definiciones de todos los sentido, pero me parece que la nomenclatura confusa. Función de los tipos parecen bastante exponencial para mí: ¿por qué son dependientes de los tipos de función (una generalización de $\rightarrow$) indicados $\Pi$ ('producto')?
Esto no parecer un tonto error: el tipo de producto $\times$ es generalizada a un dependiente del tipo de producto $\Sigma$ ('suma').
Ambos tipos son "degradado" cuando están generalizadas (exponencial del producto, producto de la suma). Evidentemente hay alguna razón detrás de esta nomenclatura, pero que va a la derecha por encima de mi cabeza.
¿Por qué Homotopy Tipo de Teoría utilizar este esquema de nomenclatura? ¿Cuál es el isomorfismo de que me estoy perdiendo?
