Langage de Programmation 2 (LP2 ) - RICM3 Cours 7 Inf 351rence de type, Makefile, R 351f

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 ...