L'inférence de type (C++, Haskell)

Voir aussi : video youtube - code source

L’inférence de types consiste à déterminer automatiquement le type d’une expression. Il s’agit d’un mécanisme qu’on trouve souvent dans les langages de programmation à typage statique, sous forme plus ou moins évoluée.

Déduction de type (C++)

En C++, on peut définir une variable avec le mot-clé auto (à la place de son type).

auto x1 = 13.37;    // double
auto x2 = 42;       // int
auto p = &x2;       // int*

Le compilateur va alors trouver le type correspondant, à partir de la valeur d’initialisation. Pour le vérifier, on peut par exemple l’afficher via typeinfo.

std::cout << "x1 " << typeid(x1).name() << std::endl;
std::cout << "x2 " << typeid(x2).name() << std::endl;
std::cout << "p  " << typeid(p).name() << std::endl;

Résultat de l’exécution :

x1 d
x2 i
p  Pi

Ici, il s’agit simplement d’un raccourci d’écriture, pour éviter au programmeur d’écrire le type concret correspondant. On parle alors de déduction de type plutôt que d’inférence de type.

En C++, on utilise auto assez classiquement pour des types un peu complexes, comme les std::function ou les itérateurs.

std::vector<int> v {13, 37};
auto it1 = v.begin();
std::vector<int>::iterator it2 = v.begin();

std::cout << "v   " << typeid(v).name() << std::endl;
std::cout << "it1 " << typeid(it1).name() << std::endl;
std::cout << "it2 " << typeid(it2).name() << std::endl;

Résultat de l’exécution :

v   St6vectorIiSaIiEE
it1 N9__gnu_cxx17__normal_iteratorIPiSt6vectorIiSaIiEEEE
it2 N9__gnu_cxx17__normal_iteratorIPiSt6vectorIiSaIiEEEE

Inférence de type (Haskell)

Dans les langages ML, l’inférence de type consiste à calculer le type le plus général correspondant à une expression donnée. Ainsi en Haskell, on écrit souvent les types des fonctions pour documenter le code mais ce n’est généralement pas obligatoire car le compilateur est capable de les inférer.

f1 :: Int -> Int
f1 x = 1 + x

f2 y = 1 + f1 y

Dans cet exemple, on a typé la fonction f1 explicitement mais pas f2. On peut facilement trouver le type de f2 d’après sa définition :

on appelle f1 sur le paramètre y, donc y doit être de type Int
le retour de f1 est un Int, auquel on ajoute 1, donc le résultat est de type Int
f2 est donc une fonction qui prend un Int et retourne un Int

*Main> :t f2
f2 :: Int -> Int

L’inférence de type est intéressante pour calculer le type le plus général possible, dans le cadre des types polymorphes. Par exemple, on a explicitement typé la fonction f1 précédente de façon à utiliser des Int. Cependant, d’après sa définition, on aurait pu utiliser aussi des Integer, des Double ou, de façon la plus générale possible, n’importe quel type de classe Num. C’est justement ce que calcule l’inférence de type. Par exemple, si on définit f3 de la même façon que f1 mais sans indiquer le type :

f3 x = 1 + x

alors le compilateur détermine bien le type :

*Main> :t f3
f3 :: Num a => a -> a

En pratique, si on active les warnings, le compilateur propose même les sigatures de fonctions manquantes, grâce à l’inférence.

$ runghc -Wall inference.hs 

inference.hs:6:1: warning: [-Wmissing-signatures]
    Top-level binding with no type signature: f2 :: Int -> Int
  |
6 | f2 x = 1 + f1 x
  | ^^

inference.hs:9:1: warning: [-Wmissing-signatures]
    Top-level binding with no type signature: f3 :: Num a => a -> a
  |
9 | f3 x = 1 + x
  | ^^

...

Typed hole (Haskell)

En plus des messages de warning précédents, on peut utiliser les “typed holes” (“trous typés”) pour écrire du code en Haskell. Il s’agit d’une fonctionnalité inspirée de Agda, qui permet de connaitre le type d’une expression avant même de l’écrire.

Pour indiquer un typed hole, on écrit le symbole _ à la place de l’expression dont on veut connaitre le type. Par exemple dans le code suivant, on veut écrire une fonction de a vers a oú a est de classe Num.

mul2 :: Num a => a -> a
mul2 x = _

Le compilateur détecte un trou correspondant à la valeur de retour de la fonction, donc de type a (avec la contrainte de type Num a). C’est ce qu’il indique dans son message d’erreur :

hole.hs:3:10: error:
    • Found hole: _ :: a
      Where: ‘a’ is a rigid type variable bound by
               the type signature for:
                 mul2 :: forall a. Num a => a -> a
               at hole.hs:2:1-23
    • In the expression: _
      In an equation for ‘mul2’: mul2 x = _
    • Relevant bindings include
        x :: a (bound at hole.hs:3:6)
        mul2 :: a -> a (bound at hole.hs:3:1)
      Constraints include Num a (from hole.hs:2:1-23)
      Valid hole fits include x :: a (bound at hole.hs:3:6)
  |
3 | mul2 x = _
  |          ^

En pratique, les typed holes peuvent aider à trouver le type d’une expression que l’on cherche à écrire. Par exemple dans le code suivant, si on veut connaitre le type de la fonction à passer à foldr, on peut mettre un trou :

allPositive :: [Int] -> Bool
allPositive = foldr _ True

puis lancer la compilation et regarder le message donné :

hole.hs:7:21: error:
    • Found hole: _ :: Int -> Bool -> Bool
    • In the first argument of ‘foldr’, namely ‘_’
      In the expression: foldr _ True
      In an equation for ‘allPositive’: allPositive = foldr _ True
    • Relevant bindings include
        allPositive :: [Int] -> Bool (bound at hole.hs:7:1)
      Valid hole fits include
        seq :: forall a b. a -> b -> b
          with seq @Int @Bool
          (imported from ‘Prelude’ at hole.hs:1:1
           (and originally defined in ‘GHC.Prim’))
  |
7 | allPositive = foldr _ True
  |                     ^

Ici, le compilateur indique qu’il attend une fonction prennant un Int et un Bool et retournant un Bool.

Exemple d’utilisation

Pour illustrer l’inférence de type et l’aide que peut apporter le compilateur pour écrire du code, imaginons qu’on veuille écrire un type List et pouvoir “fmapper” une fonction avec,

data List a
    = Nil 
    | Cons a (List a)
    deriving (Show)

main :: IO ()
main = do
    let l1 = Cons 1 $ Cons 2 Nil :: List Int
    print $ (*2) <$> l1

Pour l’instant, on a juste écrit le type et l’utilisation finale qu’on voudrait en faire. Si on compile ce code, le compilateur nous dit que notre type doit instancier la classe Functor pour pouvoir utiliser l’opérateur <$>.

list1.hs:10:13: error:
    • No instance for (Functor List) arising from a use of ‘<$>’
    • In the second argument of ‘($)’, namely ‘(* 2) <$> l1’
      In a stmt of a 'do' block: print $ (* 2) <$> l1
      In the expression:
        do let l1 = ...
           print $ (* 2) <$> l1
   |
10 |     print $ (*2) <$> l1
   |             ^^^^^^^^^^^

On peut alors commencer à écrire l’instance :

instance Functor List where

et compiler, pour connaitre la fonction à implémenter :

list2.hs:7:10: warning: [-Wmissing-methods]
    • No explicit implementation for
        ‘fmap’
    • In the instance declaration for ‘Functor List’
  |
7 | instance Functor List where
  |          ^^^^^^^^^^^^

On peut alors commencer à écrire la fonction :

instance Functor List where
    fmap = _

et utiliser un typed hole pour connaitre son type :

list3.hs:8:12: error:
    • Found hole: _ :: (a -> b) -> List a -> List b
      Where: ‘a’, ‘b’ are rigid type variables bound by
               the type signature for:
                 fmap :: forall a b. (a -> b) -> List a -> List b
               at list3.hs:8:5-8
    • In the expression: _
      In an equation for ‘fmap’: fmap = _
      In the instance declaration for ‘Functor List’
...

Le compilateur attend une fonction à deux paramètres, une fonction et une liste. On peut alors commencer à écrire un pattern-matching sur la liste et ainsi de suite jusqu’à terminer l’implémentation.

Une fois l’implémentation terminée, on peut par exemple ajouter une fonction incList qui incrémente chaque élément d’une liste donnée :

...

instance Functor List where
    fmap _ Nil = Nil
    fmap f (Cons x xs) = Cons (f x) (fmap f xs)

incList xs = (+1) <$> xs

main :: IO ()
main = do
    let l1 = Cons 1 $ Cons 2 Nil :: List Int
    print $ (*2) <$> l1
    print $ incList l1

Comme ici on utilise uniquement une liste d’entiers, on pourrait typer la fonction par incList :: List Int -> List Int. Cependant, cette fonction peut être plus générale que cela, et c’est ce qu’indique le compilateur, grâce à l’inférence :

list7.hs:12:1: warning: [-Wmissing-signatures]
    Top-level binding with no type signature:
      incList :: (Functor f, Num b) => f b -> f b
   |
12 | incList xs = (+1) <$> xs
   | ^^^^^^^

Conclusion

L’inférence de type permet de déterminer automatiquement le type d’une expression, soit par déduction simple à partir d’un type concret, soit par un calcul plus évolué dans le cas de types polymorphes.

L’inférence de type peut être utile pour alléger le code, en contrepartie d’un code moins explicite. Elle peut également assister avantageusement le développeur lors de l’écriture du code, par exemple via les typed holes.