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

pages

English

Documents

Écrit par
Pascal Lafourcade

Publié par
Thyam

Lire

Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres

pages

English

Documents

Lire

Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres

Publié par

Thyam

Langue

English

Langage de Programmation 2 (LP2)Langage de Programmation 2 (LP2)RICM3Cours 7Inférence de type, Makeﬁle, Référence, mutablePascal LafourcadePolytech2009 - 20101 / 56Langage de Programmation 2 (LP2)PlanTypage suiteTypage des exceptionsBilanUniﬁcationTerms and MessagesUniﬁcationVériﬁcation de types polymorphesSytème FSystème de Hindley-MilnerInférence de TypeConclusion2 / 56Langage de Programmation 2 (LP2)Typage suiteTypage du ﬁltrage (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 ...

Voir

Publié par

Thyam

Langue

English

LangagedeProgrammation2L(2P)

Langage de Programmation 2 RICM3 Cours 7 Inférence de type, Makeﬁle, Référence,

Pascal Lafourcade

Polytech

2009 - 2010

(LP2)

mutable

1 / 56

LnaagegderPgo

Plan

rammatino2(LP2)

Typage suite Typage des exceptions

Bilan

Uniﬁcation Terms and Messages Uniﬁcation

Vériﬁcation de types polymorphes Sytème F Système de Hindley-Milner

Inférence de Type

Conclusion

2 / 56

LnagTyapgaegdeesPuirtoergmamation2L(2P)

Typage du ﬁltrage (match)

typet=C1ofT11×  T1n1|  |CpofTp1×  Tpnp

Posons

matchEwith M=.|Ci(x1   xni)→Ei . où chaque expressionEidépend dex1  xni.

E:t

∀i1≤i≤pΓ;x17→Tp1  xni7→Tpni⊢Ei:T Γ⊢M:T

4/56

LnagyTapgaegdeesPuirtoergmaamtino2L(2P)

Typage du match

Exemple : fact II

# let rec fact n = match n with | 0 -> 1 | n -> n* (fact (n-1)) ; ; val fact : int -> int = <fun>

ngagLarogredePnoitammayT)2PL(2itsugepaedagypeToitpsnnsioceExexesptce566/

E:tE1:tE2(nb) :tE3:tE4:t T:t

(une expression)

tryEwith |ListeVide→E1 |Alarme(n,b)→E2(nb) |Not_found→E3 |Division_by_zero→E4 E,E1,E2(nb),E3,E4,  doivent avoir lemêmetype, qui est le type de l’expression entièreT.

LangBialgaendeProgrmaamitno2L(2P)

Rappel des règles de typage

Γ⊢0:int

Γ;x7→t⊢x:t Γ⊢x:tx6=y Γ;y7→u⊢x:t Γ⊢B:boolΓ⊢E1:tΓ⊢E2:t Γ⊢(ifBthenE1elseE2) :t Γ⊢A:tΓ⊢B:u Γ⊢(AB) :t×u Γ⊢E1:T1  Γ⊢En:Tn Γ⊢ {c1=E1;  cn=En}:r

Pour touti1≤i≤n,

Γ⊢E:r Γ⊢Eci:Ti

8/56

LnagBialgaendeProgrmaamtino2L(2P)

Rappel des règles de typage

E:t

Γ⊢A:t→uΓ⊢B:t Γ⊢A B:u

Γx7→t⊢E:u Γ⊢funx→E:t→u

Γ⊢A:tΓx7→t⊢B:u Γ⊢letx=AinB:u

Γx7→t⊢A:tΓx7→t⊢B:u Γ⊢let recx=AinB:u

∀i1≤i≤pΓ;x17→Tp1  xni7→Tpni Γ⊢M:T=match

⊢

Ei:T

9/65

LangBialgaendeProgrmaamitno2(L2P)

En somme, qu’est-ce qu’un type ?

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)

Procédés d’utilisation élémentaires : (principesd’élimination)

◮produits (projections, champs) ◮sommes (ﬁltrage) ◮exponentielles (application)

Symétrie introduction / élimination

10 / 56

(fnusuop,pessuopq)seu(|Oq)p,tn→E(t,p)qO→nu(finpe,nieq)|Ou(p,q)→Open,(finei)q

Chercher l’erreur... et la corriger ...par typage pousse ( Neg(Neg(Neg(Et(Vrai,Var("x"))))) ) ; ;

2/1

Lnaageg

Bilan

derPgorammation

Solution*

2(LP2)

(Analyse

par

typage)

◮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 ﬁnite set ◮Arityis a mapping fromFintoN ◮(FArity)is aranked alphabetorsignaturedenotedΣ

Deﬁnition

eMssasdneTmritnoiﬁca2)Un2(LPtionammargorPedegagnLarAtigasey

16 / 56

Voir