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
= 1 + x
f1 x
= 1 + f1 y f2 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ètrey
, doncy
doit être de typeInt
- le retour de
f1
est unInt
, auquel on ajoute1
, donc le résultat est de typeInt
f2
est donc une fonction qui prend unInt
et retourne unInt
*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 :
= 1 + x f3 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
= foldr _ True allPositive
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 ()
= do
main 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)
= (+1) <$> xs
incList xs
main :: IO ()
= do
main 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
|$> xs
12 | incList xs = (+1) < | ^^^^^^^
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.