Langages de programmation et compilation
77
pages
Français
Documents
Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres
77
pages
Français
Documents
Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres
Ecole Normale Superieure
Langages de programmation
et compilation
Jean-Christophe Filli^atre
Cours 4 / 21 octobre 2010
Jean-Christophe Filli^atre Langages de programmation et compilation 2010{2011 / cours 4 1 / 77 Typage
+
Jean-Christophe Filli^atre Langages de programmation et compilation 2010{2011 / cours 4 2 / 77 Typage
/
Jean-Christophe Filli^atre Langages de programmation et compilation 2010{2011 / cours 4 3 / 77 Typage
si j’ecris l’expression
"5" + 37
dois-je obtenir
une erreur ? (Caml)
l’entier 42 ? (Visual Basic)
la cha^ ne "537" ? (Java)
autre chose encore ?
et qu’en est-il de
37 / "5"
?
Jean-Christophe Filli^atre Langages de programmation et compilation 2010{2011 / cours 4 4 / 77 Typage
et si on additionne deux expressions arbitraires
e1 + e2
comment determiner si cela est legal, et ce que l’on doit faire le cas
echeant ?
la reponse est le typage, une analyse statique du programme qui associe
un type a chaque sous-expression, dans le but de rejeter les programmes
incoherents mais aussi de permettre la compilation
Jean-Christophe Filli^atre Langages de programmation et compilation 2010{2011 / cours 4 5 / 77 Slogan
well typed programs do not go wrong
Jean-Christophe Filli^atre Langages de programmation et compilation 2010{2011 / cours 4 6 / 77 Objectifs du typage
le typage doit ^etre decidable
le typage doit rejeter les programmes absurdes comme 1 2, dont
l’evaluation echouerait ; c’est la suret^ e du typage
le typage ne doit pas rejeter trop de programmes ...
Voir
Langages de programmation
et compilation
Jean-Christophe Filli^atre
Cours 4 / 21 octobre 2010
Jean-Christophe Filli^atre Langages de programmation et compilation 2010{2011 / cours 4 1 / 77 Typage
+
Jean-Christophe Filli^atre Langages de programmation et compilation 2010{2011 / cours 4 2 / 77 Typage
/
Jean-Christophe Filli^atre Langages de programmation et compilation 2010{2011 / cours 4 3 / 77 Typage
si j’ecris l’expression
"5" + 37
dois-je obtenir
une erreur ? (Caml)
l’entier 42 ? (Visual Basic)
la cha^ ne "537" ? (Java)
autre chose encore ?
et qu’en est-il de
37 / "5"
?
Jean-Christophe Filli^atre Langages de programmation et compilation 2010{2011 / cours 4 4 / 77 Typage
et si on additionne deux expressions arbitraires
e1 + e2
comment determiner si cela est legal, et ce que l’on doit faire le cas
echeant ?
la reponse est le typage, une analyse statique du programme qui associe
un type a chaque sous-expression, dans le but de rejeter les programmes
incoherents mais aussi de permettre la compilation
Jean-Christophe Filli^atre Langages de programmation et compilation 2010{2011 / cours 4 5 / 77 Slogan
well typed programs do not go wrong
Jean-Christophe Filli^atre Langages de programmation et compilation 2010{2011 / cours 4 6 / 77 Objectifs du typage
le typage doit ^etre decidable
le typage doit rejeter les programmes absurdes comme 1 2, dont
l’evaluation echouerait ; c’est la suret^ e du typage
le typage ne doit pas rejeter trop de programmes ...
Cours 4 / 21 octobre 2010
Jean-ChristopheFilliˆatre
Langages de programmation et compilation
´ EcoleNormaleSup´erieure
ou/c41rs
Typage
Jean-Christophe
Filliˆatre
+
Langages
de
programmation
et
compilation
2010–2011
/
cours
4
2
/
77
Typage
Jean-Christophe
Filliˆatre
/
Langages
de
programmation
et
compilation
2010–2011
/
cours
4
3
/
77
?
37 / "5"
et qu en est-il de ’
dois-je obtenir une erreur ? (Caml) l’entier 42 ? (Visual Basic) lachaıˆne"537"? (Java) autre chose encore ?
Typage
77
"5" + 37
sij’´ecrisl’expression
1/01–2104/s4urco
lar´eponseestletypage, une analyse statique du programme qui associe untypeesrammproguqseuo-s`caah,donslanprexsiesetejselrtubeered incoh´erentsmaisaussidepermettrelacompilation
commentde´terminersicelaestle´gal,etcequel’ondoitfairelecas e´cheant? ´
Typage
e1 + e2
et si on additionne deux expressions arbitraires
tspoehiFllˆitaerLangagesdeprogratammenoimoctaliponti102001–2co1/
wrong
go
programs
typed
not
do
7
well
Slogan
647/ours11/c0–20n201aˆrtLenahpFeliil-ChristoJean
le typage ne doit pas rejeter trop de programmes non-absurdes, i.e.syle`estiodsteˆtedemepyterexpressif
ipalitno02012–101/cours47/77
Objectifs du typage
letypagedoitˆetreadice´delb
le typage doit rejeter les programmes absurdes comme 1 2, dont l’´evaluation´echouerait;c’estlaeagyputedt´reˆus
gnaLertarpedsegaatmmraogomtcneioae-nJstopChrilliˆheFi
annoterseulementlesparam`etresdefonctions
fun(x:int)→lety= +(x,1)iny
annoter seulement les variables (Pascal, C, Java, etc.)
2
fun(x:int)→let(y:int) = +(x,1)iny
3
ne rien annoter⇒nineec´free,lleksa).ctetl`mpco,HmlCae(
1
touteslessous-expressionssontannot´eesparuntype
faciledeve´rifiermaistropfastidieuxpourleprogrammeur
7
4
Plusieurs solutions
847/uosr11c/naeJtni×tni)i:tn))i::int),(1(+:)(((xi:y(=)tn)tnitel→fux:n(n
unalgorithmedetypagedoitavoirlesproprie´t´esde correctione´remhtirogla’lilerslo”aui“ondpoeetsarmmrpgo:s effectivementbientyp´e
compl´etudeemhtirogtiod,a´eypntall’rslorgmapeorbteiemse:sil repondre “oui” ´
/749
Propri´ete´sattendues
et´eventuellementde principalit´eeral´en´lusgltpenoseseisxerplace´lucuopeenur:lypet possible
7c/11sruo102n02–0mpilatiotionetcoorrgmaamagegdspe
id´rons le typage de mini-ML cons e
Typage de mini-ML
1 2
typage monomorphe typagepolymorphe,inf´erencedetypes
02no2–01ipmoital10s47/71/01urco
identificateur constante (1, 2, . . .,true . .), . primitive (+,×,fst, . . .) fonction application paire liaison locale
x c op funx→e e e (e,e) letx=eine
::= | | | | | |
e
rappel
mini-ML
Jean-ChristagngdeesogprmmraehpolliFtaˆiaLer
