type inféré semble détecter une boucle infinie, mais ce qui se passe réellement?

Question

Dans Une anecdote au sujet de l'inférence de type ML , l'auteur utilise la mise en œuvre de rel="noreferrer"> comme un exercice d'apprentissage pour ML et est heureux de trouver un inférence de type « incorrect ».

  

À ma grande surprise, le compilateur fait état d'un type de

'a list -> int list

     

En d'autres termes, cette fonction de tri accepte une liste de tout type à tous et renvoie une liste d'entiers.

     

Cela est impossible. La sortie doit être une permutation de l'entrée; comment peut-il avoir un autre type? Le lecteur va sûrement trouver mon premier courant d'impulsion: je me suis demandé si je l'avais découvert un bogue dans le compilateur

     

Après avoir réfléchi un peu plus, je réalise qu'il y avait une autre façon dont la fonction pourrait ignorer son argument: peut-être parfois ne pas revenir du tout. En effet, quand je l'ai essayé, c'est exactement ce qui est arrivé. sort(nil) ne retourne nil, mais le tri toute liste non vide irait dans une boucle de récursion infinie

Lorsque Haskell traduit

split [] = ([], [])
split [x] = ([x], [])
split (x:y:xs) = (x:s1, y:s2)
  where (s1,s2) = split xs

merge xs [] = xs
merge [] ys = ys
merge xx@(x:xs) yy@(y:ys)
  | x < y     = x : merge xs yy
  | otherwise = y : merge xx ys

mergesort [] = []
mergesort xs = merge (mergesort p) (mergesort q)
  where (p,q) = split xs

GHC infère un type similaire:

*Main> :t mergesort
mergesort :: (Ord a) => [t] -> [a]

Comment le algorithme de Damas-Hindley-Milner déduire ce type ?

Answer 1

est en effet un exemple remarquable; une boucle infinie étant détectée, essentiellement, à compilation ! Il n'y a rien de spécial sur l'inférence Hindley-Milner dans cet exemple; il procède comme d'habitude.

Notez que GHC obtient correctement les types de split et merge:

*Main> :t split
split :: [a] -> ([a], [a])
*Main> :t merge
merge :: (Ord t) => [t] -> [t] -> [t]

Maintenant, quand il vient à mergesort, il est, en général, une fonction t ₁ → t ₂ pour certains types t ₁ t ₂ . Ensuite, il voit la première ligne:

mergesort [] = []

et se rend compte que t ₁ et t ₂ doit être types de listes, par exemple t ₁ = [t ₃ ] et t ₂ = [t ₄ ]. Donc mergesort doit être une fonction [t ₃ ] → [t ₄ ]. La ligne suivante

mergesort xs = merge (mergesort p) (mergesort q) 
  where (p,q) = split xs

dit-il que:

• xs doit être une entrée pour diviser, à savoir, de type [a] pour certains un (ce qui est déjà, pour a = t ₃ ).
• Alors p et q sont également de type [t ₃ ], puisque split est [a] → ([a], [a])
• mergesort p, par conséquent, (rappelons que mergesort est censé être de type [t ₃ ] → [t ₄ ]) est de type [t ₄ ].
• mergesort q est de type [t ₄ ] pour exactement la même raison.
• Comme merge est de type (Ord t) => [t] -> [t] -> [t], et les entrées dans le merge (mergesort p) (mergesort q) d'expression sont tous deux de type [t ₄ ], type t ₄ doit être dans le Ord.
• Enfin, le type de merge (mergesort p) (mergesort q) est le même que ses deux entrées, à savoir [t ₄ ]. Cela concorde avec le type connu précédemment [t ₃ ] → [t ₄ ] pour mergesort, donc il n'y a plus de déductions à faire et la partie "unification" de la algorithme Hindley-Milner est terminé. mergesort est du type [t ₃ ] → [t ₄ ] avec t ₄ dans Ord.

C'est pourquoi vous obtenez:

*Main> :t mergesort 
mergesort :: (Ord a) => [t] -> [a]

(La description ci-dessus en termes d'inférence logique est équivalent à ce que l'algorithme fait, mais la séquence spécifique d'étapes de l'algorithme suit est simplement celle donnée sur la page de Wikipédia, par exemple).

Answer 2

Ce type peut être déduit parce qu'il voit que vous passez le résultat de mergesort à merge, ce qui compare les têtes des listes avec <, qui fait partie de la classe Ord. Donc, l'inférence de type raison peut-elle qu'il doit retourner une liste d'une instance d'Ord. Bien sûr, puisqu'il récursif en fait infiniment, on ne peut rien déduire d'autre sur le type, il ne retourne pas vraiment.