Inférence de type Hindley Milner en fa #

Question

Quelqu'un peut-il expliquer étape par étape l'inférence de type dans le programme F # suivant:

let rec sumList lst =
    match lst with
    | [] -> 0
    | hd :: tl -> hd + sumList tl

Je souhaite spécifiquement voir étape par étape comment fonctionne le processus d'unification dans Hindley Milner.

Answer 1

Des trucs amusants!

Nous inventons d'abord un type générique pour sumList: x -> y

Et obtenez les équations simples: t(lst) = x; t(match ...) = y

Maintenant, vous ajoutez l'équation: t(lst) = [a] à cause de (match lst with [] ...)

Puis l'équation: b = t(0) = Int; y = b

Puisque 0 est un résultat possible du match: c = t(match lst with ...) = b

À partir du deuxième modèle: t(lst) = [d]; t(hd) = e; t(tl) = f; f = [e]; t(lst) = t(tl); t(lst) = [t(hd)]

Devinez un type (un type générique) pour hd: g = t(hd); e = g

Ensuite, nous avons besoin d'un type pour sumList, nous allons donc simplement obtenir un type de fonction sans signification pour l'instant: h -> i = t(sumList)

Nous savons maintenant: h = f; t(sumList tl) = i

Ensuite, à partir de l'addition, nous obtenons: Addable g; Addable i; g = i; t(hd + sumList tl) = g

Nous pouvons maintenant commencer l'unification:

t(lst) = t(tl) => [a] = f = [e] => a = e

t(lst) = x = [a] = f = [e]; h = t(tl) = x

t(hd) = g = i /\ i = y => y = t(hd)

x = t(lst) = [t(hd)] /\ t(hd) = y => x = [y]

y = b = Int /\ x = [y] => x = [Int] => t(sumList) = [Int] -> Int

J'ai sauté quelques étapes triviales, mais je pense que vous pouvez comprendre comment cela fonctionne.