¿Cuáles son las implicaciones prácticas de la teoría del tipo de homotopía en la programación?

Estoy empezando a aprender Haskell, después de venir de los mundos JavaScript / Ruby. Me he encontrado con https://github.com/HoTT y el libro de la teoría de tipos de homotopía , que estoy muy ansioso por leer.

Sin embargo, aprenderé los conceptos de matemática y teoría de tipos a medida que avance, por lo que parece que tomará mucho tiempo antes de entender lo que la teoría de tipos de homotopía significará para un programador en ejercicio.

¿Podría describir qué impacto tendrá la teoría del tipo de homotopía en la programación en la práctica, para un lego? Por ejemplo, ¿hará que ciertas cosas sean más fáciles de escribir? Si es así, ¿qué cosas? ¿O le permitirá hacer cosas nuevas en la programación que antes no eran posibles? Si es así, ¿qué cosas?

Gracias, tengo muchas ganas de envolver mi cabeza a un nivel más básico.

Una de las cosas poderosas que los compiladores pueden hacer durante su fase de optimización es intercambiar representaciones ineficientes por otras equivalentes. Por ejemplo, en Haskell podría usar una lista perezosa para calcular una suma de números, pero el compilador GHC Haskell reconocerá que esto es equivalente a usar la iteración con una variable temporal. De esta forma, puede programar contra una simple abstracción sobre la que es fácil razonar, mientras que su ejecutable aprovecha una representación más adecuada para la plataforma de hardware (y eso resulta mucho más difícil de razonar a escala).

Sin embargo, las equivalencias conocidas por el compilador se limitan principalmente a estructuras de datos bien conocidas e investigadas, como la fusión de flujo para listas. Puede definir sus propias equivalencias en el código fuente (usando un par de funciones de conversión que componen la identidad en cualquier dirección), pero tendría que aplicarlas manualmente, y puede ser difícil elegir el tipo correcto para usar en todos los lugares para evitar conversiones excesivas.

Ahora imaginemos un mundo en el que puedas definir "tipos inductivos superiores", por ejemplo, un mapa de búsqueda canónico. Este tipo tiene varios constructores para los diversos tipos de mapas: búsqueda binaria, AVL, rojo-negro, Trie, Patricia, etc. Junto con los constructores de datos típicos, también define un tipo de equivalencia que captura posiblemente múltiples conversiones entre estas representaciones, donde diferentes Las conversiones ofrecen diferentes dimensiones de eficiencia (es decir, tiempo frente a memoria).

¿Qué pasaría si el compilador pudiera usar esta noción para reescribir de forma transparente las representaciones de mapas, de la misma manera que puede hacerlo hoy con la fusión de listas? Mientras tanto, en su código puede trabajar con la construcción que es más simple de razonar (y hace que el trabajo de prueba sea más fácil, si se encuentra en ese entorno). Esto puede sonar como una interfaz abstracta con múltiples implementaciones, pero incluye la libertad de elegir cualquier implementación y hacer que el compilador sustituya de manera transparente a otra según sea necesario, sin afectar el significado del programa.

HoTT nos da una base teórica de tipos para justificar este mecanismo de reescritura elegante y estos tipos ricamente definidos, porque promueve la noción de equivalencia a ser equivalente a la igualdad. Queda por ver cómo esto realmente se desarrollará en la práctica, pero nos da el marco teórico en el que basar el trabajo futuro.