Langage de Programmation 2 (LP2)Langage de Programmation 2 (LP2)RICM3Cours 7Inférence de type, Makefile, Référence, mutablePascal LafourcadePolytech2009 - 20101 / 56Langage de Programmation 2 (LP2)PlanTypage suiteTypage des exceptionsBilanUnificationTerms and MessagesUnificationVérification de types polymorphesSytème FSystème de Hindley-MilnerInférence de TypeConclusion2 / 56Langage de Programmation 2 (LP2)Typage suiteTypage du filtrage (match)type t = C of T ×...T |... | C of T ×...T1 1,1 1,n p p,1 p,n1 pPosons match E with . ..M = |C (x ,...x ) → Ei 1 n ii . ..où chaque expression E dépend de x ...x .i 1 niE :t ∀i,1≤i≤p, Γ;x 7!T ...x 7!T ⊢ E :T1 p,1 n p,n ii iΓ ⊢ M :T4 / 56Langage de Programmation 2 (LP2)Typage suiteTypage du matchExemple : fact II# let rec fact n = match n with| 0 -> 1| n -> n* (fact (n-1));;val fact : int -> int = 5 / 56Langage de Programmation 2 (LP2)Typage suiteTypage des exceptionsExceptionstry E with| ListeVide→ E1| Alarme (n, b)→ E (n,b) = T (une expression)2| Not_found→ E3| Division_by_zero→ E4E, E , E (n,b), E , E , ... doivent avoir le même type,1 2 3 4qui est le type de l’expression entière T.E :t E :t E (n,b) :t E :t E :t1 2 3 4T :t6 / 566Langage de Programmation 2 (LP2)BilanRappel des règles de typageΓ ⊢ 0 : intΓ;x7!t ⊢ x :tΓ ⊢ x :t x =yΓ;y7!u ⊢ x :tΓ ⊢ B : bool Γ ⊢ E :t Γ ⊢ E :t1 2Γ ⊢ (if B then E else E ) :t1 2Γ ⊢ A :t Γ ⊢ B :uΓ ⊢ (A,B) :t×uΓ ⊢ E :T ... Γ ⊢ E ...
tryEwith |ListeVide→E1 |Alarme(n,b)→E2(nb) |Not_found→E3 |Division_by_zero→E4 E,E1,E2(nb),E3,E4, doivent avoir lemêmetype, qui est le type de l’expression entièreT.
Moyens de construction élémentaires : (principesd’introduction)
Indiquent les valeurs du type (infos non réductibles) ◮produits (ex. record Pascal, struct C, {} Ocaml, * ML) ◮sommes (sommes ML, articles avec variantes Pascal) ◮exponentielles (fonctions, tableaux)
Chercher l’erreur... et la corriger ...par typage pousse ( Neg(Neg(Neg(Et(Vrai,Var("x"))))) ) ; ;
Exercice : repousser les négations vers les extrémités* typeboolexpr= |Vrai|Faux|Varofstring|Negofboolexpr |Etofboolexpr*boolexpr|Ouofboolexpr*boolexpr
◮Thearityof a symbolf∈ FisArity(f) ◮The set of symbols of aritypis denoted byFp. ◮Elements of arity0,1 . ., .pare respectively called constants, unary, . . .p-ary symbols.
◮Fis a finite set ◮Arityis a mapping fromFintoN ◮(FArity)is aranked alphabetorsignaturedenotedΣ