Récemment, je suis devenu profondément intéressé par Haskell.
Tout en essayant d'apprendre de nouveaux concepts (par exemple le mot - clé forall et la monade ST ) et le système de types de Haskell en général, je rencontre continuellement des concepts de la théorie des catégories et du calcul lambda . Je me demande donc:
Quelles autres branches des mathématiques sont importantes pour une bonne compréhension du système de types de Haskell?
Puis-je renoncer à une étude rigoureuse de ces mathématiques et me concentrer plutôt sur certains concepts pertinents? (p. ex. quantificateurs dans le calcul lambda.) Si oui, quels concepts sont essentiels?
J'espère acquérir bientôt des types et des langages de programmation , cependant, veuillez suggérer d'autres ressources de lecture que vous jugez appropriées.
STmonade. Il est difficile d'écrire du code qui se compilera lorsque je ne comprend pas toutes les signatures de type pertinentes, j'ai donc estimé qu'il serait prudent d'améliorer ma compréhension du système de type.Réponses:
Non, vous n'avez pas besoin de prendre un livre sur la théorie des catégories pour comprendre Haskell.
J'utilise Haskell depuis quelques années et j'ai choisi une théorie des catégories par curiosité, ce n'est vraiment pas nécessaire. D'une part, c'est cool de voir comment toutes ces abstractions s'intègrent dans "la grande image", mais je ne suis pas allé "Oh mon Dieu, je dois juste en faire un profuncteur de la
Maybecatégorie à[]s et ensuite je peux enregistrer le Princesse!".Maintenant, selon ce que vous faites avec la théorie des types de Haskell est sur la clôture.
Si vous apprenez simplement haskell, n'essayez pas de comprendre toutes les nuances du système de type . S'il vous plaît ne le faites pas, c'est comme essayer d'abord d'apprendre la méta-programmation des modèles C ++. Les types fantaisistes sont d'excellents outils, mais une bonne compréhension de la programmation fonctionnelle vaut mieux que la compréhension du polymorphisme imprédicatif.
Maintenant, disons qu'après un an ou deux de Haskell, vous cherchez à comprendre chaque élément subtil du fonctionnement du système de types de Haskell, alors oui, une théorie des types pourrait être utile.
Cela vous aidera à comprendre une partie de la logique derrière la façon dont les choses fonctionnent, et c'est franchement une branche vraiment cool de l'OMI en informatique qui mérite d'être examinée. Vous pouvez choisir les pièces qui vous intéressent et en apprendre toujours une quantité décente.
Pour Haskell, en regardant STLC, les systèmes de type HM (System F) et peut-être le cube lambda (Haskell est System Fw iirc) et les types iso-récursifs. Types et langages de programmation est une excellente ressource pour commencer et couvre tous ces éléments et bien plus encore.
Si vous voulez vraiment boire le cool-aid et découvrir que vous êtes un théoricien de type en herbe, allez fouiner Agda ou Coq. Ceux-ci présentent des "types dépendants", un peu plus loin dans le cube lambda que Haskell. Les types dépendants permettent aux types de dépendre des termes. Cela signifie que les types sont suffisamment puissants pour prouver les théorèmes. Pour les curieux, l'isomorphisme curry howard sur Google devrait apporter des résultats intéressants.
la source