• Principes du typage statique
• Types de données

Partie: I
Les principes du typage

• Introduction au typage
• Quelques exemples
• Notations
• Le typage de CAML
• Modularité
• traits impératifs
• L'unification

• soit à l'exécution (typage dynamique)
• soit à la compilation (typage statique)

• détection précoce d'erreurs
• documentation, structuration (une première information sur le programme)
• facilite les optimisations (enregistrements, accès, représentations,...)
• élimination de certaines erreurs d'exécution
• sécurité du code

• le typage dynamique est plus précis (if B then 1 else 2+"a", avec B = vrai)
• le typage statique doit être conservatif
• trouver des systèmes de type les plus riches possible

• Un type est une expression d'un langage de types
• Déclarer un type = introduire un nom de type
• Définir un type = associer un nom à une exp. de type

• Typer = associer un type à une expression
• Typage fort = toute expression a un type et un seul

int addition (int x1, int x2)
{  int temp;
   temp = x1 + x2;
   return(temp); }

#let addition x1 x2 =
   let temp = x1 + x2 in
   temp;;
addition : int -> int -> int = <fun>

• vérifier que ty est un type valide pour P

• trouver un ty valide

• concision, simplicité, facilité d'écriture
• généralité plus grande des programmes
• Un algorithme fondamental de l'informatique (IA)

2 + (4 * 5)  

• des axiomes:
  P:ty
• des règles d'inférence

  P1:ty1      Pn:tyn C(P1,...,Pn):ty

• typer = construire un arbre où les feuilles sont des axiomes et les noeuds, des règles d'inférence

#let x = 1;;
x : int = 1
#let y = 2 + (4 * x);;
y : int = 6

• contient des liaisons (idf,type)
• ë (y:int)(x:int) û = Env

• liste d'association ë (x₁:ty₁),...,(x_n:ty_n) û
• une fonction d'accès acces tq:

  acces (x,ë (x1:ty1),...,(xn:tyn) û)

  = ì í î ty1 si x = x1 acces (x,ë (x2:ty2),...,(xn:tyn) û) sinon

• Types de base: unit, int, float, char, string,...
• Types construits
  - types constants déclarés
  - constructeur de type (opérateur sur les types). e.g, *
  - types paramétrés, e.g, ('a,'b) arbre
• Variables de type :a, b,... notés 'a,'b,...

• -> est associatif à droite
  (t₁ -> t₂ -> t₃ = t₁ -> (t₂ -> t₃))
• l'application est associative à gauche e₁  e₂  e₃ = (e₁  e₂)   e₃

1. Choisir une nouvelle variable de type, t, pour désigner le type de x. t est donc une inconnue.
   
   
2. Typer corps dans ë (x,t) <|  Env û. Fait apparaître des contraintes de typage (t = t₁).
3. Faire le bilan des contraintes :
   1. contraintes contradictoires : erreur de typage.
   2. variables de type toutes déterminées:
      si x : t₁ et si corps: t₂, alors
      function x -> corps: t₁ ® t₂
   3. certaines variables de type restent indéterminées: polymorphisme (plus tard)

#let x = 1;;
x : int = 1
#let y = x+x;;
y : int = 2
#let y = y+2;;
y : int = 4

1. Typage dans l'env. global courant Env
2. typage de exp
   Env  |-  exp : ty
3. le nouvel environnement global Env' = ë (idf:ty) <|  Env û

#let z = 1 in z+2;;
- : int = 3
#let y = z+1;;
Entrée interactive:
>let y = z+1;;
>        ^
L'identificateur z n'est pas défini.

1. Typage de exp1 (Env  |-  exp1 : ty₁)
2. Ajout du type obtenu à l'environnement Env_loc = ë (idf:ty₁) <|  Env û
3. Typage de exp2 dans Env_loc (Env'  |-  exp2 : ty₂)
4. L'environnement global est inchangé

#let rec fact1 = function n ->
     if n <= 0 then 1 
     else n * fact1 (n-1);;
fact1 : int -> int = <fun>

1. Choisir deux nouvelles variables de type t₁ et t₂ pour désigner le type de f puis étendre Env Env' = ë (f:t₁ ® t₂), (x:t₁)<|  Env û
   
   
2. typer corps (Env'  |-  corps : ty₂)
3. Faire le bilan des contraintes (t₁ = t₁ et t₂ = t₂)

#let app_tab f t =
   for i = 0 to vect_length t - 1 do
     t.(i) <- f (t.(i))
   done;;
app_tab : ('a -> 'a) -> 'a vect -> unit = 
<fun>
#let ajout n t = 
   app_tab (function x -> x+n) t;;
ajout : int -> int vect -> unit = <fun>
#let not_tab t = 
   app_tab (function x -> not x) t;;
not_tab : bool vect -> unit = <fun>

• généralité du code, concision
• réutilisabilité (bibliothèques)

#let id = function x -> x;;
id : 'a -> 'a = <fun>
#id true,id 1;;
- : bool * int = true, 1

#(function f -> f true,f 1) (function x -> x);;
Entrée interactive:
>(function f -> f true,f 1) (function x -> 
x);;
>                        ^
Cette expression est de type int,
mais est utilisée avec le type bool.

1. Env  |-  exp1 : t₁
   
   
2. Si exp1 NON expansive, généraliser t₁ en st₁ = generaliser_Env(t₁), sinon st₁ = t₁
3. Ajout du type obtenu à l'environnement
4. ë (x:st₁) <|  Env û  |-  exp2 : ty₂
5. L'environnement global est inchangé

#let id = function x -> x;;
id : 'a -> 'a = <fun>
#let f = id id;;
f : '_a -> '_a = <fun>
#let g = function x -> (id id) x;;
g : 'a -> 'a = <fun>

#2 + 3;;
- : int = 5
#prefix +;;
- : int -> int -> int = <fun>
##open "float";;
#prefix +;;
- : float -> float -> float = <fun>
#1.2 + 1.3 ;;
- : float = 2.5
#2 + 3;;
Entrée interactive:
>2 + 3;;
>^
Cette expression est de type int,
mais est utilisée avec le type float.

#add_int 2 3;;
- : int = 5
##close "float";;
#2 + 3;;
- : int = 5
#1.2 + 1.3 ;;
Entrée interactive:
>1.2 + 1.3 ;;
>^^^
Cette expression est de type float,
mais est utilisée avec le type int.

1. Un corps : définitions (types, fonctions, constantes, etc.) regroupées dans un texte nommé mod.ml.
2. Une interface d'exportation nommée mod.mli qui définit les déclarations visibles à l'extérieur: contient des déclarations de types et de valeurs (nom, type).
3. Pour l'importateur: module = env. de typage (utilisé au cours du typage)
4. si aucune interface mod.mli n'est définie, toutes les déclarations sont exportées.

1. D : liaisons des déclarations du pgm. en cours
2. O : liaisons des modules ouverts
3. C : modules connus du système

1. D : vide
2. O : modules de la librairie "core" => man. de ref.
3. C : modules connus du système

1. C : les liaisons déclarées dans les interfaces mod.mli connues du système sont accessibles avec la notation mod__idf.
2. ouvrir mod: placer les liaisons de mod au début de O.
3. Si idf de mod déjà lié dans O => masquage de la liaison antérieure, qui reste accessible avec la notation complète.
4. Aucun masquage des liaisons de D.

1. Quelle est la syntaxe des déclarations globales? Où doivent-elles être placées?
2. Même question avec les déclarations locales.
3. Si ce langage est typé, comment est faite la vérification/inférence des types.
4. Si ce langage offre des bibliothèques, y a-t-il compilation séparée?
5. Comment sont gérés les noms des bibliothèques?

#let counter = ref 0;;
counter : int ref = ref 0
#let add_counter n =
   counter := !counter + n;;
add_counter : int -> unit = <fun>
#let afficher mess =
   print_string mess;
   print_newline ();;
afficher : string -> unit = <fun>
#exception Division_par_zero;;
L'exception Division_par_zero est 
définie.
#let division x y = 
   if y = 0 then raise Division_par_zero
   else x / y;;
division : int -> int -> int = <fun>

• s(t₁ ® t₂) = s(t₁) ® s(t₂)
  
• s(t₁ * t₂) = s(t₁) * s(t₂)
  
• s(int) = int

• Déclaration du type des identificateurs/synthèse du type
• Vérification/inférence
• Typage fort: une expression a un type unique
• Garanties apportées par le typage fort

• surcharge
• sous-typage, objets
• modules

Partie: II
Les types de données

• Introduction
• types de base
• types produit
• types somme
• types récursifs

• contruire des structures complexes à partir de structures de base
• les types donnent une information sur ces structures

• elle manipulent (construisent/ accèdent) ces structures de données.
• le filtrage est un moyen de raisonner ``par cas'' sur la forme de ces structures.

• int, bool,...

#fst;;
- : 'a * 'b -> 'a = <fun>
#snd ;;
- : 'a * 'b -> 'b = <fun>

#let fst = function (x,y) -> x;;
fst : 'a * 'b -> 'a = <fun>
#let snd = function (x,y) -> y;;
snd : 'a * 'b -> 'b = <fun>
#let acceder3 = function (x,y,z,t) -> z;;
acceder3 : 'a * 'b * 'c * 'd -> 'c = 
<fun>
#let double_zero = function
       (0,0) -> true
     | (x,y) -> false;;
double_zero : int * int -> bool = <fun>

#type enfant = {nom : string ; age : int};;
Le type enfant est défini.
#let simon = {nom = "Simon" ; age = 9};;
simon : enfant = {nom = "Simon"; age = 9}

#let nom {nom = n;age = a} = n;;
nom : enfant -> string = <fun>
#let nom {nom = n} = n;;
nom : enfant -> string = <fun>
#let nom x = x.nom;;
nom : enfant -> string = <fun>

#let anniv = function x -> 
   {nom = x.nom ; age = x.age + 1};;
anniv : enfant -> enfant = <fun>
#(anniv simon);;
- : enfant = {nom = "Simon"; age = 10}
#simon;;
- : enfant = {nom = "Simon"; age = 9}

#type societe = {nom : string; numero : int};;
Le type societe est défini.
#let nom2 x = x.nom;;
nom2 : societe -> string = <fun>

• gauche : A    ® A Å B
• droit : A    ® A Å B

#type color = Coeur | Pique | Carreau | Trefle ;;
Le type color est défini.
#type carte = Dam of color
            | Peti of int*color
            | Jok ;;
Le type carte est défini.

#let valeurfoo = function
   | Dam _  -> 20
   | Peti (10, c) -> 10
   | Peti (x, y) -> 
       if x = 9 & y = Coeur then 11 else 0
   | Jok  -> 1 ;;
valeurfoo : carte -> int = <fun>
#type unites = V of float | H  of float;;
Le type unites est défini.
#let distance_parcourue =
   function (V x, H y) -> x *. y ;;
Entrée interactive:
>  function (V x, H y) -> x *. y ;;
>  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Attention: ce filtrage n'est pas 
exhaustif.
distance_parcourue : unites * unites -> 
float = <fun>
#distance_parcourue (V 25.0, H 4.0);;
- : float = 100.0

• C est un constructeur de type
• i désigne un entier
• x, une variable

#deriv "x" mon_exp;;
- : exp = P (C 1, P (C 0, C 0))

#type sans_val = C of sans_val * sans_val ;; 
Le type sans_val est défini.

• Un programme = des données + des fonctions
• filtrage = raisonnement par cas sur la structure de ces données

• représentation de ces données
• qu'est ce qu'une valeur?
• comment obtenir la valeur d'une expression?

Ce document a été traduit de L^AT_EX par H^EV^EA.