Quais são as implicações práticas da teoria dos tipos de homotopia na programação?

Estou apenas começando a aprender Haskell, depois de vir dos mundos JavaScript / Ruby. Encontrei https://github.com/HoTT e o livro Homotopy Type Theory , que estou muito ansioso para ler.

No entanto, aprenderei os conceitos de matemática e teoria dos tipos à medida que for desenvolvendo, portanto, parece que demorará muito tempo para eu entender o que a teoria dos tipos de homotopia significará para um programador praticante.

Você poderia descrever qual o impacto que a teoria do tipo homotopia terá na programação na prática, para um leigo? Por exemplo, isso tornará certas coisas mais fáceis ou mais fáceis de escrever? Se sim, quais coisas? Ou permitirá que você faça coisas novas em programação que antes não eram possíveis? Se sim, quais coisas?

Obrigado, muito ansioso para envolver minha cabeça em um nível mais básico.

Uma das coisas poderosas que os compiladores são capazes de fazer durante sua fase de otimização é trocar representações ineficientes por equivalentes. Por exemplo, em Haskell, você pode usar uma lista lenta para calcular uma soma de números, mas o compilador GHC Haskell reconhecerá que isso é equivalente ao uso da iteração com uma variável temporária. Dessa forma, você pode programar com base em uma abstração simples e fácil de raciocinar, enquanto o executável aproveita uma representação mais adequada à plataforma de hardware (e isso é muito mais difícil de raciocinar em escala).

No entanto, as equivalências conhecidas pelo compilador são restritas principalmente a estruturas de dados conhecidas e pesquisadas, como fusão de fluxo para listas. Você pode definir suas próprias equivalências no código-fonte (usando um par de funções de conversão que compõem a identidade em qualquer direção), mas é necessário aplicá-las manualmente, e pode ser complicado escolher o tipo certo para uso em todos os lugares para evitar conversões excessivas.

Agora vamos imaginar um mundo onde você possa definir "tipos indutivos mais altos", digamos um mapa de pesquisa canônico. Esse tipo possui vários construtores para os vários tipos de mapas: pesquisa binária, AVL, preto-vermelho, Trie, Patricia, etc. Juntamente com os construtores de dados típicos, você também define um tipo de equivalência capturando possivelmente várias conversões entre essas representações, onde diferentes as conversões oferecem dimensões variáveis ​​de eficiência (tempo versus memória).

E se o compilador fosse capaz de usar essa noção para reescrever transparentemente representações de mapa, da mesma maneira que pode fazer hoje com a fusão de listas? Enquanto isso, no seu código, você começa a trabalhar com a construção que é mais simples de raciocinar (e facilita o trabalho de prova, se você estiver em um ambiente assim). Isso pode soar como uma interface abstrata com várias implementações, mas inclui a liberdade de escolher qualquer implementação e fazer com que o compilador substitua de forma transparente outra conforme necessário, sem afetar o significado do programa.

O HoTT nos fornece uma base teórica do tipo para justificar esse mecanismo de reescrita sofisticado e esses tipos ricamente definidos, porque promove a noção de equivalência em ser equivalente à igualdade. Resta ver como isso realmente acontecerá na prática, mas nos fornece a estrutura teórica sobre a qual basear o trabalho futuro.