Vérification de type et types récursifs (Écriture du combinateur Y dans Haskell / Ocaml)

Lorsque vous expliquez le combinateur Y dans le contexte de Haskell, il est généralement noté que l'implémentation simple ne vérifie pas le type dans Haskell en raison de son type récursif.

Par exemple, à partir de Rosettacode :

The obvious definition of the Y combinator in Haskell canot be used
because it contains an infinite recursive type (a = a -> b). Defining
a data type (Mu) allows this recursion to be broken.

newtype Mu a = Roll { unroll :: Mu a -> a }

fix :: (a -> a) -> a
fix = \f -> (\x -> f (unroll x x)) $ Roll (\x -> f (unroll x x))

Et en effet, la définition «évidente» ne tape pas check:

λ> let fix f g = (\x -> \a -> f (x x) a) (\x -> \a -> f (x x) a) g

<interactive>:10:33:
    Occurs check: cannot construct the infinite type:
      t2 = t2 -> t0 -> t1
    Expected type: t2 -> t0 -> t1
      Actual type: (t2 -> t0 -> t1) -> t0 -> t1
    In the first argument of `x', namely `x'
    In the first argument of `f', namely `(x x)'
    In the expression: f (x x) a

<interactive>:10:57:
    Occurs check: cannot construct the infinite type:
      t2 = t2 -> t0 -> t1
    In the first argument of `x', namely `x'
    In the first argument of `f', namely `(x x)'
    In the expression: f (x x) a
(0.01 secs, 1033328 bytes)

La même limitation existe dans Ocaml:

utop # let fix f g = (fun x a -> f (x x) a) (fun x a -> f (x x) a) g;;
Error: This expression has type 'a -> 'b but an expression was expected of type 'a                                    
       The type variable 'a occurs inside 'a -> 'b

Cependant, dans Ocaml, on peut autoriser les types récursifs en passant le -rectypescommutateur:

   -rectypes
          Allow  arbitrary  recursive  types  during type-checking.  By default, only recursive
          types where the recursion goes through an object type are supported.

En utilisant -rectypes, tout fonctionne:

utop # let fix f g = (fun x a -> f (x x) a) (fun x a -> f (x x) a) g;;
val fix : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b = <fun>
utop # let fact_improver partial n = if n = 0 then 1 else n*partial (n-1);;
val fact_improver : (int -> int) -> int -> int = <fun>
utop # (fix fact_improver) 5;;
- : int = 120

Étant curieux de connaître les systèmes de types et l'inférence de types, cela soulève des questions auxquelles je ne suis toujours pas en mesure de répondre.

• Tout d'abord, comment le vérificateur de type propose-t-il le type t2 = t2 -> t0 -> t1? Ayant trouvé ce type, je suppose que le problème est que le type ( t2) se réfère à lui-même sur le côté droit?
• Deuxièmement, et peut-être le plus intéressant, quelle est la raison pour laquelle les systèmes de type Haskell / Ocaml interdisent cela? Je suppose qu'il y a une bonne raison car Ocaml ne le permettra pas non plus par défaut même s'il le peut gérer des types récursifs si on lui donne le -rectypescommutateur.

Si ce sont des sujets vraiment importants, j'apprécierais des pointeurs vers la littérature pertinente.

Tout d'abord, l'erreur GHC,

GHC tente d'unifier quelques contraintes avec x, tout d'abord, nous l'utilisons comme une fonction afin

x :: a -> b

Ensuite, nous l'utilisons comme valeur pour cette fonction

x :: a

Et enfin, nous l'unissons avec l'expression d'argument d'origine afin

x :: (a -> b) -> c -> d

Devient maintenant x xune tentative d'unification t2 -> t1 -> t0, cependant, Nous ne pouvons pas unifier cela car il faudrait unifier t2, le premier argument de x, avec x. D'où notre message d'erreur.

Ensuite, pourquoi pas les types récursifs généraux. Eh bien, le premier point à noter est la différence entre les types récursifs équi et iso,

• équi-récursif sont ce que vous attendez mu X . Type est exactement équivalent à le développer ou le plier arbitrairement.
• Les types iso-récursifs fournissent une paire d'opérateurs foldet unfoldqui replient et déplient les définitions récursives des types.

Désormais, les types équi-récursifs semblent idéaux, mais sont absurdement difficiles à obtenir correctement dans les systèmes de types complexes. Cela peut en fait rendre la vérification de type indécidable. Je ne connais pas tous les détails du système de types d'OCaml, mais les types entièrement équirécursifs dans Haskell peuvent faire en sorte que le vérificateur de typage boucle de manière arbitraire en essayant d'unifier les types, par défaut, Haskell s'assure que la vérification de type se termine. De plus, dans Haskell, les synonymes de type sont stupides, les types récursifs les plus utiles seraient définis commetype T = T -> () , mais sont presque immédiatement insérés dans Haskell, mais vous ne pouvez pas aligner un type récursif, c'est infini! Par conséquent, les types récursifs dans Haskell nécessiteraient une refonte énorme de la façon dont les synonymes sont traités, probablement pas la peine de mettre même comme une extension de langue.

Les types iso-récursifs sont un peu pénibles à utiliser, vous devez plus ou moins explicitement dire au vérificateur de type comment plier et déplier vos types, rendant vos programmes plus complexes à lire et à écrire.

Cependant, cela est très similaire à ce que vous faites avec votre Mutype. Rollest plié et unrollse déplie. Donc, en réalité, nous avons des types iso-récursifs intégrés. Cependant, les types équi-récursifs sont tout simplement trop complexes, donc des systèmes comme OCaml et Haskell vous obligent à passer des récurrences via des points de correction de niveau type.

Maintenant, si cela vous intéresse, je recommande les types et les langages de programmation. Ma copie est ouverte sur mes genoux pendant que j'écris ceci pour m'assurer d'avoir la bonne terminologie :)

Dans OCaml, vous devez passer -rectypescomme paramètre au compilateur (ou entrer #rectypes;;dans le niveau supérieur). En gros, cela désactivera le "contrôle des événements" pendant l'unification. La situation The type variable 'a occurs inside 'a -> 'bne sera plus un problème. Le système de types sera toujours "correct" (son, etc.), les arbres infinis qui surgissent comme types sont parfois appelés "arbres rationnels". Le système de type s'affaiblit, c'est-à-dire qu'il devient impossible de détecter certaines erreurs de programmation.

Voir ma conférence sur lambda-calcul (à partir de la diapositive 27) pour plus d'informations sur les opérateurs de points fixes avec des exemples dans OCaml.