Les types (que l'on dit simples)

Planche : 2

A: Qu’est-ce qu’un type ?
B: PCF simplement typé.
C: Sémantique dénotationelle.

Quelques problèmes à l’exécution

Par exemple, (Fun x -> x) + 1
Ou bien, 1 2 (un appliqué à deux)
Et même, Ifz (Fun x -> x+1) Then 0 Else 1

Et en effet,

additionner des fonctions (impossible),
appliquer des entiers (impossible),
tester si une fonction vaut 0 (possible, mais bizarre, ne présage rien de bon pour la suite).

Ce qui se passe à l’exécution

Soit le cas (Fun x -> x)+1.

Dans par exemple la machine ASEC.

let rec run a s e c = match a,s,c with
…
| Int n2,Val (Int n1)::s,IOp ADD::c ->
run (Int (n1+n2)) s e c
…
| _,_,_ -> raise Error

Donc : lancer une exception (erreur détectée).

Ou dans le code compilé :

#IOp (Add)
addl %eax,0(%esp)
popl %eax

Donc : calculer n’importe quoi (erreur non-détectée).

Ce que dit la sémantique

De par exemple « 1 2 ».

À grands pas : rien.
À petits pas : terme bloqué (forme normale qui n’est pas une valeur).
Dénotationelle : c’est quoi déjà ?

L’erreur peut être peu évidente

Let fact =
Fix fact -> Fun n ->
Ifz n Then 1 Else n * fact (n-1) In
Let r = Ifz 100-fact 10 Then 0 Else (Fun x -> x) In
r 1

L’exécution échoue (application de 0 à 1).

On doit pouvoir détecter cette erreur à l’usine (compilation), avant qu’elle ne se produise chez le client (exécution).

Sémantique dénotationnelle

Associer à un terme t (syntaxe) un “vrai” truc t = [[t]].

Vrai veut dire disons,

Avec les moyens reconnus légaux (cf. Marx).
Vrais (cf. Platon).

Simplifions : il existe ℕ et une “vraie” fonction est une fonction de A dans B où A et B sont des ensembles.

On peut donc essayer d’associer :

À 0, l’entier (∈ ℕ) 0.
À Fun x -> x+1, la fonction de ℕ dans ℕ, qui à x associe x+1.
À Fun x -> x, la fonction de ? dans ?, qui à x associe x.
À Fun x -> x x ? (Là, ça va pas être possible.)

Deux problèmes, une solution

Les problèmes :

Ne livrer que des programmes sans erreurs (sans erreurs du style « 1 2 »).
Définir la sémantique dénotationelle de PCF.
(Éviter les paradoxes du genre X = { x ∣ x ∉x}.)

La solution : obliger le programmeur à spécifier le domaine de définition des fonctions.

Une solution radicale, mais qui va fonctionner.

Un nouveau PCF

t	::==	`n`
	\|	x
	\|	t₁ `op` t₂
	\|	t₁ t₂
	\|	Fun (x`:`T) `->` t
	\|	Fix (x`:`T) `->` t
	\|	Let x `=` t₁ In t₂

Cf. définition de méthode en Java:

int f(int x) { … }

La même chose en Caml

Syntaxe abstraite du nouveau PCF (dans T.Ast).

Mais qu’est-ce que T.Type.t (T) ?

Planche : 11

Ensembles de définition des fonctions

Pour éviter « 1 2 » et « (Fun x -> x+1)+2 »), il doit suffire de séparer entiers et fonctions.

Pour autoriser

Let f = Fun x -> x+1 In f 1 + 2

Et interdire

Let f = Fun x -> x 1 In f 1 + 2

Il faut être un peu plus détaillé, les deux types de f

Nat -> Nat (Nat -> Nat) -> Nat

Planche : 12

Algèbre des types

Les types sont décrits ainsi :

Nat est un type.
Si A et B sont des types, alors A -> B est un type.

Autrement dit :

ℕ ∈ T

A ∈ T B ∈ T

A -> B ∈ T

Ou encore :

type t = Nat | Arrow of t * t

C’est le language des types (simples), il n’a pour le moment aucune sémantique.

Planche : 13

Types et ensembles

Idée évidente pour la sémantique : des ensembles.

Selon notre programme de vérifier les types à la compilation, les types ne peuvent pas être des ensembles quelconques.

Ex. Pourquoi pas un type ℕ^* ? (Nat^*) Ça serait bien commode :

Let div = Fun (x:Nat) -> Fun (y:Nat^*) -> x / y

Et bien non,

Typer div 100 (fact 10-100) demande de prouver que la valeur de fact 10 est > 100, c’est beaucoup demander à un compilateur.
Quel type donner à la soustraction ?

Tant pis : l’usine (compilateur) peut livrer des programmes qui divisent par zéro.

Planche : 14

Contrôle à l’usine

Écrire Fun (x:A) -> t n’empêche pas les erreurs.

(Fun (x:Nat) -> x 1) 2

Mais cela permet de définir facilement un sous-ensemble des termes : les termes bien typés.

L’ensemble des termes bien typés est défini par une relation

E ⊢ t:A

(Le terme t possède le type A dans l’environnement E.)

Dans le cas d’un environnement vide on abrège

t:A

(Le terme t a le type A.)

Planche : 15

Exemples

Fun (x:Nat) -> x 1

Mal typé, car x de type Nat est appliqué (à 2).

Fix (x:Nat) -> x + 1

Bien typé.

Fix (f:Nat) ->
Fun (n:Nat) ->
Ifz n Then 1 Else 2 * f (n-1)

Mal typé, car f de type Nat est appliqué (à n-1). On aurait pu écrire:

Fix (f:Nat -> Nat) ->
Fun (n:Nat) ->
Ifz n Then 1 Else 2 * f (n-1)

Planche : 16

Définition inductive de E ⊢ t:A

E ⊢ n:Nat

E(x) = A

E ⊢ x:A

E ⊢ t₁:Nat E ⊢ t₂:Nat

E ⊢ t₁ op t₂:Nat

E ⊢ t₁:Nat E ⊢ t₂:A E ⊢ t₃:A

E ⊢ Ifz t₁ Then t₂ Else t₃:A

E ⊢ t₁:A -> B E ⊢ t₂:A

E ⊢ t₁ t₂:B

E ⊕ [x:A] ⊢ t:B

E ⊢ (Fun (x:A) -> t):A -> B

E ⊕ [x:A] ⊢ t:A

E ⊢ (Fix (x:A) -> t):A

E ⊢ t₁:A E ⊕ [x:A] ⊢ t₂:B

E ⊢ Let x = t₁ In t₂:B

Planche : 17

Typage de la puissance de deux

[⋯; n:Nat] ⊢ n:Nat E ⊢ 1:Nat E ⊢ t₂:Nat

[f:Nat -> Nat,n:Nat] ⊢ Ifz n Then 1 Else t₂:Nat

[f:Nat -> Nat] ⊢ (Fun (x:Nat) -> Ifz ⋯):Nat -> Nat

∅ ⊢ (Fix (f:Nat -> Nat) -> t):Nat -> Nat

∅ ⊢ 100:Nat

∅ ⊢ (Fix (f:Nat -> Nat) -> t) 100:Nat

Avec E ⊢ t₂:Nat prouvé comme suit :

E ⊢ 2:Nat

E ⊢ f:Nat -> Nat

E ⊢ n:Nat E ⊢ 1:Nat

E ⊢ n-1:Nat

E ⊢ f (n-1):Nat

[f:Nat -> Nat,n:Nat] ⊢ 2 * f (n-1):Nat

N.B. Inutile de calculer 2¹⁰⁰.

Planche : 18

La relation E ⊢ t:A

Ressemble très fortement à une sémantique « à grand pas ».

Pour cela, on l’appelle :

Sémantique statique (car valable au moment de la compilation).
Interprétation abstraite, car elle est une abstraction de la sémantique, qui calcule des ensembles de valeurs et non plus des valeurs.

Calculer A tel que t:A est surtout vérifier le type de t, car on ne découvre (infère) pas franchement A.

Planche : 19

Décidabilité

Avec des règles aussi précises,

On écrit facilement un programme qui étant donnés E et t trouve A tel que E ⊢ t:A ou échoue.
Et de plus A est unique.
On dit que la relation « ∅ ⊢ t:A », notée « t:A », est décidable et non-ambigüe.

C’est ce que nous ferons en TP.

open T
exception Error

val check : (Var.t * Type.t) list -> Ast.t -> Type.t
(* L'appel 'check E t' envoie A tel que E ⊢ t:A,
ou lance Error si il n'existe pas de tel A *)

Planche : 20

Correction du typage statique

On veut exprimer que si un terme est bien typé (à la compilation), alors il ne se produit pas d’erreurs (de type) lors de l’exécution.

Sémantique à petit pas. Deux gros lemmes :
- subject reduction, c-à-d, si t:A et t → t′, alors t′:A.
  Cela se montre par induction sur la dérivation t:A.
- progress, c’-à-d, si t:A et t n’est pas une valeur, alors t n’est pas en forme normale.
  Cela se montre en détaillant les termes bloqués et en montrant qu’ils ne sont pas typables.
- Il vient ce Théorème (Correction du typage statique), t:A entraîne l’absence d’erreurs (de type) à l’exécution.

Planche : 21

Correction, à grand pas

Une méthode pas satisfaisante, prouver:

(t:A ∧ t↪v) ⇒ v:A

Un peu court, car termes qui bouclent et erreurs de type sont confondus.

On ajoute une « valeur » wrong qui exprime une erreur de type, et des règles de propagation.

t₁↪n

t₁ t₂↪wrong

t₁↪wrong

t₁ t₂↪wrong

t₂↪wrong

t₁ t₂↪wrong

…

On obtient alors une formulation plus précise, qui entraîne:

(t:A ∧ t↪v) ⇒ v ≠ wrong

Planche : 22

Une dernière réflexion

Le typage A:t garantit l’absence d’erreurs de type à l’exécution.

La réciproque est bien entendu fausse.

(Ifz 0 Then 0 Else (Fun x -> x))+1

Cette incomplétude est un prix à payer pour le le typage statique.

Pourquoi ? À cause de l’indécidabilité de l’arrêt : il n’existe pas d’algorithme qui permet de décider si P (bien typé) termine.

Soit P bien typé (et donc exempt d’erreur) et :

(Ifz P Then 0 Else (Fun x -> x)) + 1

Un erreur se produit à l’exécution entraîne P termine (et P s’évalue n différent de zéro).

Planche : 23

Un dernier thérorème

Si t:A et que t ne contient pas Fix, alors toutes les réductions issues de t terminent (Tait).

Corollaire :

Le terme (Fun x -> x x) (Fun x -> x x) n’est pas typable.
Aucun codage du point fixe n’est typable. Disons qu’un codage du pt. fixe est un terme Y avec
Y t →^* t (Y t)

On peut alors coder Fix f -> t comme Y (Fun f -> t).
Pour un exemple, cf poly (Exercice 2.10).

Planche : 24

Sémantique dénotationelle

Maintenant que les termes contiennent des types, il devient possible d’associer une fonction des mathématiques à toute fonction PCF.

Commençons par associer (fonction [[·]]) un ensembles à chaque type de PCF.

[[Nat]] = ℕ

[[A -> B]] = [[A]] → [[B]]

(où E₁ → E₂ est l’ensemble des fonctions de E₁ vers E₂).

On a alors six règles évidentes.

[[n]] = n

[[t₁ op t₂]] = [[t₁]] op[[t₂]]

[[Ifz t₁ Then t₂ Else t₃]] = [[t₂]] si [[t₁]] est 0, ou [[t₃]] si [[t₁]] est n ≠ 0

Planche : 25

Sémantique dénotationelle triviale

À t:A on associe [[t]] dans [[A]]. ([[t]] est une valeur sémantique, un elément de ∪_{A ∈ T} [[A]]).

La sémantique des termes ouverts est relative à un environnment sémantique E des variables vers les valeurs sémantiques,

[[x]]_E = E(x)
[[Let x = t₁ In t₂]]_E = [[t₂]]_{E ⊕ [x=[[t₁]]_E]}
[[Fun (x:A) -> t]]_E, la fonction qui à tout v de [[A]], associe [[t]]_{E ⊕ [x=v]}.
[[t₁ t₂]]_E = [[t₁]]_E([[t₂]]_E)

Avec une définition à peine modifiée (qui explicite le type des valeurs sémantiques de l’environnement), on verrait que si t:A, alors [[t]] existe et ∈ [[A]], mais bon.

Planche : 26

Frustration

Toute cette dépense théorique pour des paraphrases en italiques !

Mais, la sémantique triviale laisse de côté deux questions.

Que vaut [[1/0]] ? Faux problème, cela vaut error, on décide error ∈ [[A]] pour tout A, et on modifie les règles pour propager cette erreur.
Et le point fixe ? Vrai problème.
La tentation est grande de définir [[Fix (x:A) -> t]] comme point fixe de
[[Fun (x:A) -> t]]

Mais cela ne va pas se faire tout seul.

Planche : 27

Point fixe

En PCF on peut écrire le terme Fix (x:A) -> t (du moment que l’on a [x:A] ⊢ t:A).

On se se préocupe pas de l’existence du point fixe de [[Fun (x:A) -> t]]. Par exemple :

T₁ = Fix (x:Nat) -> x+1

Or, il n’existe pas d’entier x tel que x = x+1.

Si on revient à la sémantique opérationnelle, on avait :

(Fix (x:A) -> t) → [Fix (x:A) -> t\x]t

Et donc :

T₁ → T₁+1 → (T₁+1)+1 → ⋯

Pour compléter les valeurs sémantiques on donne la valeur ⊥ à ce terme (terme de type Nat, qui ne termine pas).

Planche : 28

Une vérification

On a donc posé [[Nat]] = ℕ ∪ {⊥}.

Si on complète les quatres règles des opérations

[[t₁ op t₂]] = ⊥, si [[t₁]] ou [[t₂]] est ⊥

Alors ⊥ est l’unique point fixe de [[Fun (x:Nat) -> x+1]]

De même, [[Fun (x:Nat) -> x]] (function qui à x entier associe x) avait plusieurs point fixes 0, 1, 2,…

Maintenant, cette fonction (qui à x ∈ [[Nat]] associe x) a un pt. fixe de plus ⊥.

Et c’est celui là que l’on veut pour [[Fix (x:Nat) -> x]] (termine pas).

Points fixes de [[Fun (x:Nat) -> x+x]] ? ⊥ et 0. Valeur de [[Fix (x:Nat) -> x+x]] ? ⊥

Planche : 29

Comment choisir son point fixe

Ordre de Scott sur le domaine [[Nat]].

Ordre faiblement complet ? Oui !

On veut le plus petit point fixe.

Il existe bien pour toutes les fonctions croissantes et continues de [[Nat]] dans [[Nat]].

Ce qui est le cas de [[Fun (x:Nat) -> x+1]] etc.

Planche : 30

Et dans le cas général…

Définition revue des domaines sémantiques :

[[Nat]] = ℕ ∪ { ⊥ }
[[A -> B]] fonctions croissantes et continues de [[A]] dans [[B]].

L’ordre sur [[A -> B]] est défini point à point, f ≤ g sisi ∀ x ∈ [[A]], f(x) ≤ g(x).

Il y a un plus petit elt : la fonction qui à x ∈ [[A]] associe ⊥_B (notée ⊥_{A -> B}).

Cette relation est faiblement complète (permutation de limites).

Tous les termes de type A s’interprètent bien dans [[A]] (continuité).

La valeur de Fix (x:A) -> t est définie comme le plus petit point fixe de [[Fun (x:A) -> t]].

Planche : 31

Qu’est-ce que ça veut dire en pratique ?

Fonction puisssance de deux :

Let P =
  Fix (p:Nat -> Nat) ->
    Fun (n:Nat) ->
      Ifz n Then 1 Else 2 * p (n-1)

Noté Fix (p:Nat -> Nat) -> t.

Pour avoir la valeur du terme ci-dessus, on calcule le pppf de Φ = [[Fun (p:Nat) -> t]].

Le plus pppf de Φ est la limite de la suite (a_k) = (Φ^k(⊥_{Nat -> Nat})).

a₀	⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥	⋯
a₁	⊥	1	⊥	⊥	⊥	⊥	⊥	⊥	⋯
a₂	⊥	1	2	⊥	⊥	⊥	⊥	⊥	⋯
a₃	⊥	1	2	4	⊥	⊥	⊥	⊥	⋯
a₄	⊥	1	2	4	8	⊥	⊥	⊥	⋯
a₅	⊥	1	2	4	8	16	⊥	⊥	⋯
a₆	⊥	1	2	4	8	16	32	⊥	⋯

Car par exemple : a₆(5) = 2 * a₅(4) (en sautant quelques étapes).

Planche : 32

Mise en relation des sémantiques

Il y a un théorème (pas facile) :

[[t]] = n ⇔t↪n

Ce théorème s’applique-t-il à l’évaluation en appel par nom ou par valeur ?

Considérer :

Let k = Fun (x:Nat) -> Fun (y:Nat) -> y In
Let loop = Fix (n:Nat) -> n In
k 0 loop

Cela vaut [[y]]_{[loop=⊥, y=0]} qui vaut 0.

Donc c’est appel par nom.

Planche : 33

À quoi ça sert ?

C’est beau de savoir que l’on programme de vraies fonctions.

À prouver des théorèmes. Par ex.

On ne peut pas programmer en PCF typé, la fonction g qui prend f:Nat -> Nat en argument, et renvoie 0 si f 0 vaut zéro et 1 autrement.

Soit donc g de [[(Nat -> Nat) -> Nat]] telle que ci-dessus.

Considérer f₀ = [[Fun x:Nat -> 0]], f₁ = [[Fun x:Nat -> 1]], On ⊥_{Nat -> Nat} ≤ f₀ et ⊥_{Nat -> Nat} ≤ f₁. Soit (g croissante) g(⊥_{Nat -> Nat}) = ⊥ C.Q.F.D.

Bon on joue sur les mots, voir Exercice 5.11 pour un exemple plus sérieux.

Planche : 34

TP, vérification de type.
La prochaine fois, inférence de type.

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

Planche : 1

Planche : 2

Planche : 3

Quelques problèmes à l’exécution

Planche : 4

Ce qui se passe à l’exécution

Planche : 5

Ce que dit la sémantique

Planche : 6

L’erreur peut être peu évidente

Planche : 7

Sémantique dénotationnelle

Planche : 8

Deux problèmes, une solution

Planche : 9

Un nouveau PCF

Planche : 10

La même chose en Caml

Planche : 11

Ensembles de définition des fonctions

Planche : 12

Algèbre des types

Planche : 13

Types et ensembles

Planche : 14

Contrôle à l’usine

Planche : 15

Exemples

Planche : 16

Définition inductive de E ⊢ t:A

Planche : 17

Typage de la puissance de deux

Planche : 18

La relation E ⊢ t:A

Planche : 19

Décidabilité

Planche : 20

Correction du typage statique

Planche : 21

Correction, à grand pas

Planche : 22

Une dernière réflexion

Planche : 23

Un dernier thérorème

Planche : 24

Sémantique dénotationelle

Planche : 25

Sémantique dénotationelle triviale

Planche : 26

Frustration

Planche : 27

Point fixe

Planche : 28

Une vérification

Planche : 29

Comment choisir son point fixe

Planche : 30

Et dans le cas général…

Planche : 31

Qu’est-ce que ça veut dire en pratique ?

Planche : 32

Mise en relation des sémantiques

Planche : 33

À quoi ça sert ?

Planche : 34