Cours 2

Htmligure
Version & licenses
Creative Commons License

Les types

Guyslain
Thursday, 21 July 2016

Retour au sommaire.

Ce cours porte particulièrement sur les types. Les types sont très riches en OCaml, et permettent d'exprimer de nombreuses propriétés des programmes directement au niveau des types. Le choix des types guide une part cruciale du développement ; souvent le programme se dérive très simplement une fois les types bien choisis. Cela a néanmoins un prix : comprendre et apprivoiser cette richesse pour l'utiliser au mieux. En fait, d'ici la fin du semestre, c'est quasiment ce qui va nous occuper exclusivement. Nous commençons par rappeler des généralités vus au cours précédent. Nous parlerons ensuite de polymorphisme, c'est-à-dire la possibilité d'utiliser des valeurs quelque soit leur type. Puis nous introduirons les types paramétrés, qui dépendent d'autres types. Finalement, nous étudierons les grandes familles de types paramétrés.

Généralités.

En OCaml, comme dans d'autres langages de programmation, les types ont deux rôles principaux :

  1. en définissant de nouveaux types, le programmeur donne des représentations adaptées des données ou de l'état d'un système, ce qui simplifie la tâche de développement,
  1. ils permettent de vérifier le bon usage des arguments d'une fonction, des méthodes d'une classe, et ainsi détecter de nombreuses erreurs dès la compilation. De même ils permettent de documenter l'usage des fonctions, dans la documentation d'une API.

OCaml est un langage typé : les abstractions possèdent toute un type, correctement défini. De fait tout expression possède un type, et même les modules et les objets ont des types.

Nous avons précédemment introduit plusieurs types :

  • int le type des entiers,
  • float le type des flottants,
  • bool le type des booléens,
  • char le type des caractères,
  • string le type des chaînes de caractères,
  • dom -> im le type des fonctions du type domvers le type im
  • (left * right) le type des paires d'un élément du type left et d'un élément du type right

Les deux derniers types de cette liste sont en fait des familles infinies de types, tous différents. Plus généralement, on peut définir d'autres familles de types de la même façon, c'est ce que nous appelons types paramétrés, et une grande partie de ce cours va porter sur les types paramétrés et leur usage.

L'inférence de type

OCaml est un langage avec inférence de type : le compilateur déduit le type des variables selon l'utilisation qui en est faite, il n'est pas nécessaire de lui déclarer le type des variables qui sont définies. Attention à ne pas confondre cela avec la croyance que les variables n'ont pas de types : toutes les variables ont un type, même s'il n'est pas écrit dans le programme.

Par exemple, voici une fonction pour additionner deux entiers :

  1. let sum a b = a + b

Il n'est pas précisé quel est le type des arguments a et b. Mais le compilateur détecte l'utilisation de l'addition sur ces deux variables, il en déduit donc intelligemment que a et b ont le type int. Il en déduit aussi que sum a le type int -> int -> int.

S'il n'existe pas de types pour chaque abstraction, qui rende le programme typable, l'inférence échoue et la compilation aussi. Le programme est simplement non-correct.

On aurait pu écrire la même fonction, en annotant les types des arguments :

  1. let sum (a:int) (b:int) = a + b

Le symbole : sert en OCaml a indiqué le type d'une valeur, avec la syntaxe (value : value_type). Cette syntaxe peut être utilisée à peu près n'importe où dans une expression.

On peut même annoter le type de ce que retourne la fonction, ou le type de la fonction elle-même, en utilisant la bonne syntaxe :

  1. let sum : int -> int -> int = fun a b -> a + b
  2. let sum (a:int) (b:int) : int = a + b

En pratique, le plus couramment on n'annote pas les types des variables et arguments,sauf dans le but de rendre le code plus facile à lire. Si le nom d'une variable ne suffit pas à comprendre quel est son type, c'est une bonne idée de le préciser par une annotation (ou de trouver un nom de variable plus adapté).

Un autre usage des annotations est de trouver la provenance d'une erreur de type. Les annotations servent d'indication au compilateur, qui peut ainsi donner des messages d'erreurs plus précis si le programme contient des erreurs de types.

Les erreurs de types.

Si un programme n'est pas typable, la compilation échoue avec un message d'erreur. Le message est toujours de la même forme :

  1. Error: This expression has type some_type
  2. but an expression was expected of type some_other_type

avec les numéros de ligne et de colonne de l'expression désigné. L'erreur se comprend ainsi :

  • le compilateur a inféré que l'expression indiquée a le type some_type. Si c'est une variable, il l'a décidé par rapport à une autre utilisation de cette variable qui a été faite auparavant, par exemple son initialisation si c'est une variable expression-locale. Sinon, il l'a déduit de la forme même de l'expression, par exemple si c'est le résultat de l'application d'une fonction il peut l'avoir déduit du type de la fonction.
  • le compilateur a aussi inféré que la façon dont est utilisée cette expression exige qu'elle soit de type some_other_type. Par exemple l'expression indiquée est argument d'une fonction, donc doit avoir le type de l'argument.
  • comme les deux types sont différents, ce n'est pas possible : il n'y a pas de conversions entre types en OCaml. L'inférence échoue donc.

Pour résoudre ces erreurs, il faut :

  1. déterminer lequel des types some_type ou some_other_type correspond à votre intention.
  2. si c'est some_type, l'erreur est à l'endroit indiquée, dans l'utilisation qui est faite de l'expression écrite. Vérifiez la façon dont cette expression est utilisée.
  3. si c'est some_other_type, l'erreur est probablement avant, à un endroit où l'expression peut déjà s'être fait attribué un type, ou au moins une contrainte sur son type.

Regardons quelques exemples.

  1. utop # let some_float = 1̲ +. 2.;;
  2. Error: This expression has type int
  3. but an expression was expected of type float

Le compilateur désigne 1 comme l'expression problématique. On veut calculer une addition flottante, donc int semble être le mauvais type. C'est donc l'expression indiquée qui est erronée. Bien sûr, le litéral flottant s'écrit 1. !

  1. utop # let some_int = 1̲ +. 2;;
  2. Error: This expression has type int
  3. but an expression was expected of type float

Dans ce cas, l'expression a le type int, comme nous le souhaitons. Par contre l'interprète indique qu'il faut un flottant à cet endroit. Effectivement, 1 est l'argument de +., qui demande un flottant. L'erreur est donc d'avoir utilisé l'addition flottante +. à la place de l'addition entière +.

  1. utop # let rec fact n =
  2. if n = 0. then 1
  3. else n̲ * fact (n-1);;
  4. Error: This expression has type float
  5. but an expression was expected of type int

Ici on se doute que n devrait être de type int. Il faut donc comprendre pourquoi l'interprète croit que n a le type float. Pour cela, on vérifie les autres usages de la variable n. Ainsi, dans la condition du if, n est comparé à 0. qui est un flottant, donc l'interprète en déduit que n est flottant (l'égalité compare des valeurs de même type). Il faut donc remplacer 0. par 0.

  1. utop # let rec fact n =
  2. if n = 0 then 1.
  3. else n * (̲f̲a̲c̲t̲ ̲(̲n̲-̲1̲)̲);;
  4. Error: This expression has type float
  5. but an expression was expected of type int

Cette fois ce n'est pas normal que fact (n-1) soit considéré comme un flottant. Il a donc déduit que fact : some_type -> float. Cela peut paraître surprenant puisque nous sommes en train de définir fact, comment connait-il déjà son type ? En y réfléchissant, le type de retour de factest le type de l'expression des branches de la conditionnelle if then else, qui doivent être identiques. Or, l'expression pour then est clairement en flottant, c'est de là qu'il en a déduit que fact produit un flottant. Il suffit donc de remplacer le littéral 1. par 1.

C'est l'erreur de type classique sur les conditionnelles (et plus généralement les branchements, nous verrons des formes de branchements plus élaborée par la suite). Chaque branche doit produire des expressions de même types. C'est la raison pour laquelle oublier la branche else produit une erreur de type :

  1. utop # let rec fact n =
  2. if n > 0 then n̲ ̲*̲ ̲f̲a̲c̲t̲ ̲(̲n̲-̲1̲)̲;;
  3. Error: This expression has type int
  4. but an expression was expected of type unit

Si une branche est manquante, on considère que l'expression associé ne retourne rien, et le type de rien est unit, ce qui explique le message d'erreur. Le diagnostic est simplement : la branche else est manquante. Rappelons la règle : toujours faire des if avec les deux branches !

  1. utop # let pred n = n -. 1.;;
  2. val pred : float -> float = <fun>

  3. utop # let rec fact n =
  4. if n = 0 then 1
  5. else n * fact (pred n̲);;
  6. Error: This expression has type int
  7. but an expression was expected of type float

Dans cet exemple nous souhaitons effectivement que n soit de type int. Le problème vient donc de l'usage qui est fait de n. La fonction pred devraient travailler sur les entiers, et non sur les flottants, il faut donc la corriger.

Dans des exemples plus sophistiqués, pour les erreurs de types dont l'origine est difficile à trouver, une stratégie simple est d'utiliser des annotations de type sur les variables du programme. Ceci indique explicitement au compilateur les intentions du programmeur, et permet donc de repérer plus tôt et plus précisément les erreurs de types. Il ne faut donc pas hésiter à utiliser des annotations dans les programmes complexes.

Trouver la raison d'une erreur de type n'est pas toujours facile, l'erreur n'étant pas toujours à l'endroit indiqué, et lorsque les types deviennent complexes, comprendre même pourquoi il y a une erreur demande de la réflexion. Il est cependant réconfortant de savoir que dans un langage au typage moins strict, une erreur similaire aurait typiquement provoqué une erreur de segmentation à l'exécution, et trouver son origine aurait été bien plus difficile. Même s'il est frustrant de constater et de corriger toutes les erreurs de types indiquées lors de la compilation, il s'agit globalement d'un gain de temps sur toute la conception du programme.

Retour au sommaire.