Récemment, j'ai commencé mes études en théorie des types / systèmes de types et Lambda Calculus.
J'ai déjà lu sur le calcul lambda simple typé dans le style Church and Curry. Le dernier est également connu sous le nom de système d'attribution de type (TA).
Je pense aux relations entre TA et Hindley-Milner (HM), le système dans des langues comme ML et Haskell.
Le livre Lambda-Calculus and Combinators: An Introduction (Hindley) dit que TA est polymorphe (pag. 119). Est-ce le même sens du polymorphisme dans des systèmes comme HM et System-F?
Le TA aurait la forte propriété de normalisation, il n'est donc pas complet. Les langages utilisant le système HM sont complets, Haskell par exemple. Il doit donc en être ainsi que le système HM autorise des termes comme la boucle infiniepour recevoir un type. Est-ce correct ou il me manque quelque chose?
Quoi qu'il en soit, j'aimerais connaître la relation entre TA et HM.
la source
Réponses:
Le système F et son sous-système HM ont un ancien type pour la quantification universelle:
que le système de Hindley / Seldin n'a pas. Voilà la principale différence.
Désormais, le système F n'a pas d'inférence de type décidable, et HM est un moyen de combiner l'inférence de type avec un polymorphisme paramétrique raisonnablement expressif. HM y parvient en autorisant uniquement la quantification universelle la plus externe, c'est-à-dire que tous les types sont de la forme
oùτ est sans quantificateur (et n≥0 ). HM propose un système de règles garantissant que seuls les programmes pouvant être saisis de cette manière sont admissibles. Ceci est réalisé par "let-polymorphisme". Le système de Hindley / Seldin ne fait rien de tout cela. Plus tard, dans le chapitre 13, Hindley / Seldin présente des systèmes de type pur (PTS), dont le système F est un cas spécial. Je ne sais pas si HM peut être exprimé en PTS.
La question d'une forte normalisation est orthogonale. Les systèmes F et HM normalisent fortement, mais cela peut facilement être résolu en introduisant des combinateurs à point fixe ou similaire. L'article principal Schémas de type pour les programmes fonctionnels par L. Damas et R. Milner déclare même ceci: " Par exemple, la récursivité est omise car elle peut être introduite en ajoutant simplement l'opérateur polymorphe à point fixe ... " L'introduction des points fixes , rendant le système Turing complet, ne pose aucun problème du point de vue de l'inférence de type.
la source