Je commence tout juste à apprendre Haskell, après être venu des mondes JavaScript / Ruby. J'ai rencontré https://github.com/HoTT et le livre The Homotopy Type Theory , que j'ai très hâte de lire.
Cependant, j'apprendrai les concepts mathématiques et la théorie des types au fur et à mesure, il semble donc qu'il faudra beaucoup de temps avant de comprendre ce que la théorie des types d'homotopie signifiera pour un programmeur pratiquant.
Pourriez-vous décrire quel impact la théorie des types d'homotopie aura sur la programmation en pratique, pour un profane? Par exemple, rendra-t-il certaines choses plus faciles à écrire? Si oui, quelles choses? Ou cela vous permettra-t-il de faire de nouvelles choses dans la programmation qui n'étaient pas possibles auparavant? Si oui, quelles choses?
Merci, très impatient d'envelopper ma tête autour de lui à un niveau plus basique.
la source
Réponses:
L'une des choses puissantes que les compilateurs sont capables de faire pendant leur phase d'optimisation est d'échanger des représentations inefficaces contre des représentations équivalentes. Par exemple, dans Haskell, vous pouvez utiliser une liste paresseuse pour calculer une somme de nombres, mais le compilateur GHC Haskell reconnaîtra que cela équivaut à utiliser l'itération avec une variable temporaire. De cette façon, vous pouvez programmer contre une abstraction simple et facile à raisonner, tandis que votre exécutable profite d'une représentation mieux adaptée à la plate-forme matérielle (et qui s'avère beaucoup plus difficile à raisonner à grande échelle).
Cependant, les équivalences connues du compilateur sont principalement limitées à des structures de données bien connues et recherchées, telles que la fusion de flux pour les listes. Vous pouvez définir vos propres équivalences dans le code source (en utilisant une paire de fonctions de conversion qui composent l'identité dans les deux sens), mais vous devrez les appliquer manuellement, et il peut être difficile de choisir le bon type à utiliser dans tous les endroits afin d'éviter des conversions excessives.
Imaginons maintenant un monde où vous pouvez définir des "types inductifs supérieurs", par exemple une carte de recherche canonique. Ce type a plusieurs constructeurs pour les différents types de cartes: recherche binaire, AVL, rouge-noir, Trie, Patricia, etc. Avec les constructeurs de données typiques, vous définissez également un type d'équivalence capturant éventuellement plusieurs conversions entre ces représentations, où différentes les conversions offrent différentes dimensions d'efficacité (c.-à-d. le temps par rapport à la mémoire).
Et si le compilateur était capable d'utiliser cette notion pour réécrire de manière transparente les représentations cartographiques, de la même manière qu'il peut le faire aujourd'hui avec la fusion de listes? Pendant ce temps, dans votre code, vous travaillez avec la construction la plus simple à raisonner (et facilite le travail de vérification, si vous êtes dans un tel environnement). Cela peut ressembler à une interface abstraite avec plusieurs implémentations, mais cela inclut la liberté de choisir n'importe quelle implémentation et de faire en sorte que le compilateur en remplace une autre de manière transparente selon les besoins, sans affecter la signification du programme.
HoTT nous donne une base théorique de type pour justifier ce mécanisme de réécriture sophistiqué et ces types richement définis, car il promeut la notion d'équivalence à être équivalente à l'égalité. Il reste à voir comment cela se concrétisera dans la pratique, mais cela nous donne le cadre théorique sur lequel baser les travaux futurs.
la source