Planche 1
Cours 2
Langages fonctionnels typés
Jean-Jacques.Levy@inria.fr
http://jeanjacqueslevy.net

secrétariat de l'enseignement:
Catherine Bensoussan
cb@lix.polytechnique.fr
Laboratoire d'Informatique de l'X
Aile 00, LIX
tel: 34 67

http://w3.edu.polytechnique.fr/informatique

Planche 2
Références
Planche 3
Plan

  1. Déclarations
  2. Portée -- Liaison lexicale
  3. Interpréteurs et environnements
  4. Types
  5. Typage statique, typage dynamique
  6. Vérification de type
  7. Extension avec des listes
Planche 4
PCF et déclarations

Termes
M, N, P ::= ... voir cours précédent
  | let  x = M in N déclaration

Exemples

let  x = 3 in x + 1
let  x = 2 in let  y = x + 1 in 2 × x + y
let  f = l x. x× x + 1 in f 4 + f 5
let  f = l x. x× x + 1 in f (f x) let  f = l x. x× x + 1 in   let  g = l f.l x. f(f x)  in g f x
let  fact = µ f.l x. ifz x then 1 else x × f(x-1)   in   fact 5

Planche 5
Déclarations

La notation anonyme des fonctions est souvent cachée dans l'instruction let , on écrit plutôt
let  f  x = M in N pour let  f = l x.M in N

La déclaration let  n'est pas non plus nécessaire puisqu'on a
let  x = M in N identique à (l x.N)M

mais on verra plus tard des différences dans les lois de typage.

L'instruction let  f = l x. x× x + 1 in f 4 + f 5

correspond en ML à 

let f = function x -> x*x+1 in f 4 + f 5 ;;
ou en Java à 

class Test {
  static int f (int x) { return x * x + 1; }
  public static void main (String[ ] args) { 
    System.out.println (f(4) + f(5)); 
  }
}
Planche 6
Blocs --- Portée d'une déclaration 


int f (int x) 
{
    return x*x + 1;
}

int main (int argc, char *args[])
{
    return f(4) + f(5);
}
Certains langages comme Pascal ou Modula ont des blocs plus structurés autorisant la définition de fonctions locales dans les fonctions. Les blocs peuvent être emboîtés, comme en PCF où un let  peut être contenu dans tout sous-terme.

Dans let  x = M in N, la déclaration de la variable locale x porte sur tout N.

Planche 7
Variables locales -- globales

let  fact =
l x.
let  f =
µ f.
l x.
l r.
ifz   x then r else f (x-1) (x*r)
r
 
x
 
f
 
in
f   x   1
f
 
x

in
fact  
 
5
fact

En PCF, un bloc correspond à la portée de toute déclaration.

Planche 8
PCF avec déclarations récursives

Termes
M, N, P ::= ... voir cours précédent
  | letrec  x = M in N déclaration récursive

Nous n'utiliserons pas cette extension, car on peut écrire
letrec  x = M in N pour let  x = µ x.M in N

Exercice 1Ecrire l'expression de µ x.M en terme de letrec . L'appliquer au cas de la factorielle.

Planche 9
Syntaxe abstraite de PCF avec déclaration 


type nom = string;;

type term =
...
| Let of nom * term * term;;
Variables libres
FV(let  x = M in N) = FV((l x.N)M) = FV(M) È (FV(N) - {x})

Exercice 2Calculer FV(letrec  x = M in N)

Variables liées
BV(let  x = M in N) = BV((l x.N)M) = BV(M) È BV(N) È {x}

Planche 10
Valeurs (inchangé)
V,V' ::= x variable
  | l x.M abstraction
  |
 
n
constante entière

Substitution et réductions

On définit (let  y = M in N)[x \ P] à partir de ((l y.N)M)[x \ P], ainsi que ses réductions.
a
 
 
let  x = M in N º let  x'= M in N [x \ x'] (x' ÏFV(N))
b
 
 
let  x = V in N ® N [x \ V]

Remarque Exercice 3Expliciter (let  y = M in N)[x \ P]
Exercice 4Donner la règle de réduction de letrec 

Planche 11
Sémantique opérationnelle de l'appel par valeur

On étend la SOS (structural operational semantics) de l'appel par valeur pour tenir compte du let 
|- l x.M = l x.M
|- M[x \ µ x.M] = V
|- µ x.M = V
|- M = l x.P    |- N = V'    |- P [x \ V'] = V
|- MN = V
|-
 
n
=
 
n
|- M = m    |- N = n
|- M Ä N = mÄ n
|- M = 0    |- M = V
|- ifz M then N then N' = V
|- M = n    |- N = V'    (n¹ 0)
|- ifz M then N then N' = V'
|- M = V'    |- N [x \ V'] = V
|- let  x = M in N = V

Planche 12
Environnements et SOS bigstep

On donne un deuxième argument à la fonction d'évaluation, l'environnement r qui décrit la liaison des variables.

r est une liste d'association entre les noms des variables locales et leur valeur.

On redéfinit les règles de l'appel par valeur
r |- l x.M = l x.M[r]
r,x=V |- M = V
r |- µ x.M = V
r |- M = l x.P[r']    r |- N = V'    r', x= V' |- P = V
r |- MN = V
r |-
 
n
=
 
n
r |- M = m    r |- N = n
r |- M Ä N = mÄ n
r|- P = 0    r|- M = V
r|- ifz P then M then N = V
r|- P = n    r|- N = V    (n¹ 0)
r|- ifz P then M then N = V'
r |- M = V'    r, x=V' |- N = V
r |- let  x = M in N = V
r, x=V |- x = V

Planche 13
Environnements

On peut aussi voir r comme une fonction des noms dans les valeurs.
V ::=
x |
 
n
| (l x.P)[r]
valeurs
r ::= (x1 = V1), (x2=V2), ··· (xn=Vn) xi distincts (n ³ 0)
avec r [x \ V] (x) = V et r [x \ V] (y) = r(y) sinon.

r |- l x.M = l x.M[r]
r |- x = r(x)         
r[x \ V] |- M = V
r |- µ x.M = V
r |- M = l x.P[r']    r |- N = V'    r'[x \ V'] |- P = V
r |- MN = V
r |-
 
n
=
 
n
r |- M = m    r |- N = n
r |- M Ä N = mÄ n
r|- P = 0    r|- M = V
r|- ifz P then M then N = V
r|- P = n    r|- N = V    (n ¹ 0)
r|- ifz P then M then N = V

Planche 14
Environnements et récursivité

La règle pour µ x.M est imprécise. Par exemple |- µ x.x = V pour tout V. Dans cette règle, la valeur est définie en fonction d'un environnement qui est récursif.

On peut voir r comme une fonction des noms dans les valeurs.
V ::=
x |
 
n
| (l x.P)[r]
valeurs
r ::= (x1 = V1), (x2=V2), ··· (xn=Vn) xi distincts (n ³ 0)
    | r | µ r.r

On modifie certaines des règles.
r |- µ x.
 
n
=
 
n
r |- µ x.l y.M = l y.M [µ r.r[x \ l y.M[r]] ]
r[r \ µ r.r] |- x = V
µ r.r |- x = V
r |- x = r(x)

Planche 15
Exercices sur les environnements

Exercice 5Trouver la règle du letrec 

Exercice 6Trouver une solution avec des valeurs récursives.

Exercice 7Refaire la SOS sans environnements récursifs pour la règle µ, mais deux règles pour l'application.

Exercice 8(en TD) Ecrire en ML la fonction eval M rho calculant V si r |- M = V et où rho est une liste d'association représentant l'environnement r.

Exercice 9Faire la SOS pour l'appel par nom avec des environnements, et calculer eval M rho.

Planche 16
Types

Planche 17
Langages de programmation typés

En PCF, si on écrit 2   1 ou 2(1), c'est une erreur. De même, pour (l x.x) + 1, ou (l f. l g.l x.f(g x))(l x.x 1)(l x.2)

De manière générale, seules les opérations bien définies sur certains domaines sont autorisées. Diffère de l'assembleur (ou de C) où toutes les adresses mémoire sont (ou peuvent être considérées comme) aussi des nombres.

Credo Typage Þ sureté

Langages fortement typés Caml, Java, Scheme, Lisp

Langages typés Pascal

Langages faiblement typés C, C++

Langages non typés Assembleur

Planche 18
Intérêt des types

Planche 19
Types en PCF
t,t' ::= int les entiers naturels N
  | t ® t' les fonctions de T dans T'

Termes de PCF typé
M, N, P ::= x variable
  | l x :  t.M abstraction
  | MN application
  |
 
n
constante entière
  | M Ä N Ä Î {+,-,×,÷ }
  | ifz M then N then N' conditionnelle
  | µ x :  t.M définition récursive
  | let  x :  t = M in N déclaration

Abréviation t ® t' ® t'' pour t ® (t' ® t'')

Planche 20
Exemples

let  x :  int = 3 in x + 1
let  x :  int = 2 in let  y :  int = x + 1 in 2 × x + y
let  f :  int ® int = l x : int. x× x + 1 in f 4 + f 5
let  f :  int ® int = l x : int. x× x + 1 in f (f x)
let  f :  int ® int = l x : int. x× x + 1 in
let  g :  (int ® int) ® int ® int = l f :  int ® int.l x :  int. f(f x) in
g f x
let  fact :  int ® int = µ f :  int ® int.
l x  : int. ifz x then 1 else x × f(x-1) in
fact 5

Remarques Plus uniforme de garder l'annotation de type à l'introduction de chaque nouvelle variable.

Planche 21
Règles de typage
r, x :  t |- x  :  t
r, x :  t |- M  :  t'
r |- l x :  t.M  :  t ® t'
r |- M  :  t ® t'   r |- N  :  t
r |- MN  :  t'
r |-
 
n
 :  int
r |- M  :  int    r |- N  :  int
r |- M Ä N  :  int
r |- M  :  int    r |- N  :  t    r |- N'  :  t
r |- ifz M then N then N'  :  t
r, x :  t |- M  :  t
r |- µ x :  t.M  :  t
r|- M  :  t    r, x :  t |- N  :  t'
r|- let  x  :  t = M in N  :  t'

Exercice 10Donner la règle du letrec 

Planche 22
Quelques propriétés

Théorème 3 [unicité] Si r |- M :  t et r |- M :  t', on a t = t'

Théorème 4 [subject reduction] Si r |- M :  t et M ® N, on a r |- N :  t

Disons que M ® err si M contient un sous-terme de la forme n N, (l x.M) Ä n ou m Ä (l x.N).

Corollaire 5 [sureté] Si r |- M :  t et si M ®* N, alors N ¬ ®err

Théorème 6 [progression] Si |- M :  t, alors soit M est une valeur, soit M ® N.

Dans le lambda calcul (c'est à dire sans la règle µ),

Théorème 7 [normalisation forte] Si r |- M :  t, toutes les réductions issues de M sont finies.

Ce dernier théorème est particulièrement dur à démontrer. Une démonstration a été faite par Sanchis 60, une autre par Tait et Martin-Löf.

Planche 23
Correspondance de Curry-Howard

Soient I = l x.x, K = l x.l y.x et S=l x.l y.l z.xz(yz).

Les types de I, K et S sont de la forme
|- I :  a ® a
|- K :  a ® b ® a
|- S : (a® b ® g) ® (a ® b) ® a ® g

Or 3 premiers axiomes de la logique propositionnelle sont
|- A É A
|- A É B É A
|- (AÉ B É C) É (A É B) É A É C

Types « Formules
Termes « Preuves !!!

Planche 24
Présentation de PCF typé à la Church

Termes sans annotations de type. Les règles de typage sont
|- r, x :  t |- x  :  t
r, x :  t |- M  :  t'
r |- l x.M  :  t ® t'
r |- M  :  t ® t'   r |- N  :  t
r |- MN  :  t'
r |-
 
n
 :  int
r |- M  :  int    r |- N  :  int
r |- M Ä N  :  int
r |- M  :  int    r |- N  :  t    r |- N'  :  t
r |- ifz M then N then N'  :  t
r, x :  t |- M  :  t
r |- µ x.M  :  t
r|- M  :  t    r, x :  t |- N  :  t'
r|- let  x = M in N  :  t'
Exercice 11Montrer qu'alors le théorème d'unicité n'est plus vrai.

Planche 25
Typage statique -- Typage dynamique

Il est facile d'écrire un programme qui vérifie ou calcule le type d'une expression. On dit que l'expression est typée statiquement. Au cours de l'exécution, on peut oublier les types et exécuter surement et efficacement du PCF.

Certains langages (Lisp, Scheme) ne vérifient les types qu'à l'exécution (Typage dynamique). Les termes autorisés sont plus généraux, mais il n'y a aucune garantie d'absence d'erreur à l'exécution. Rien de dramatique ne peut se passer. L'exécution est plus lente. (Une partie de Java fonctionne ainsi).

Exercice 12Donner un exemple de terme de PCF non typable statiquement, mais typable dynamiquement (sans erreur d'exécution).

Exercice 13Ecrire un vérificateur de type pour PCF typé.

Planche 26
Extension des types avec des listes
t,t' ::= int les entiers naturels N
  | t ® t' les fonctions de T dans T'
  | list(t) listes de T

Termes de PCF typé avec listes
M, N, P ::= ... cf. PCF typé
  | hd M tête de liste
  | tl M queue de liste
  | nil liste vide
  | M :: N constructeur
  | ifnil M then N then N' cond. sur les listes

Exercice 14Sait-on écrire simplement des règles de typage pour ce langage?

Planche 27
En TD

La prochaine fois

This document was translated from LATEX by HEVEA.