El ejemplo típico de tipo inductivo más alto (HIT) es el círculo $S^1$ que se describe muy bien aquí . Entiendo que los HIT son convenientes si quieres hacer teoría de homotopía dentro de la teoría de tipos. ¿Pero qué aporta el informático? ¿Existen estructuras de datos interesantes que no podrían definirse sin un HIT?
Respuesta
¿Demasiados anuncios?
Buena pregunta. Para empezar debo ser claro que creo Golpes son, probablemente, mucho más interesante para un homotopy teórico que a un científico de la computación. Sin embargo, parece que ellos no están totalmente desprovisto de interés para un científico de la computación.
Una clase general de las aplicaciones es la construcción de la verdadera cocientes, donde se tiene una estructura de datos en la que el mismo "objeto real" tiene múltiples representaciones; por lo representan como un éxito usted puede agregar real igualdades entre las dos representaciones, de modo que cualquier función definida en esta estructura de datos debe necesariamente el respeto que la igualdad ("representación independiente").
Además, aquí están algunos de los mensajes de los homotopy tipo de teoría de blog sobre temas que puedan ser de interés para los científicos de la computación:
