Quelles fonctions le système F ne peut-il pas calculer?

Dans cet article de wikipedia sur l'exhaustivité de Turing, il déclare que:

Le calcul lambda non typé est Turing complet, mais de nombreux calculs lambda typés, y compris le système F, ne le sont pas. La valeur des systèmes dactylographiés est basée sur leur capacité à représenter la plupart des programmes informatiques typiques tout en détectant plus d'erreurs.

Quel est un exemple d'une fonction calculable totale non calculable par le système F ?

De plus, puisque hindley-milner est:

Une restriction du système F

à cause du fait que:

la vérification de type est indécidable pour une variante de style Curry du système F, c'est-à-dire qui manque d'annotations de frappe explicites.

Est-ce à dire que le calcul lambda sous-jacent aux systèmes de type hindley-milner n'est pas aussi complet?

Si cela est vrai, étant donné que haskell est clairement complet et que nous savons que sa base est le calcul lambda et le système de type hindley-milner, quelles fonctionnalités qui ne sont pas présentes dans le calcul lambda sont ajoutées afin de compléter la turing haskell?

$F$$\mathbb{N}\rightarrow\mathbb{N}$$\mathbb{N}$$\forall X.\ X\rightarrow (X\rightarrow X)\rightarrow X$$\mathbb{N}\rightarrow\mathbb{N}$$\mathrm{HA}_2$

$T$$F$$\mathrm{eval}:\mathbb{N}\rightarrow\mathbb{N}$$t$$F$$t$. La preuve implique une variante de l'astuce de diagonalisation utilisée pour l'indécidabilité du problème d'arrêt. Andrej l'explique magnifiquement ici .

$\lambda$$F$ $\lambda$

$Y$$Y$

Notez qu'il existe d'autres fonctionnalités qui rendent Haskell Turing complet, mais elles ne sont généralement pas considérées comme faisant partie du langage de base, par exemple des références à des fonctions, des types de données illimités, etc.

Il est quelque peu trompeur de dire que le système de frappe de Haskell est "le système de type hinley-milner". Les types de Haskell sont beaucoup plus puissants, y compris, entre autres, les types de type supérieur. En effet, le système de frappe est si puissant que vous pouvez intégrer des langages de programmation complets de Turing dans le système de frappe, voir ici . Ce n'est pas la seule raison du pouvoir de Haskell, Cody en a mentionné d'autres.