cours sur les inférence de type

Description

-1-INF 554 Luc MarangetInf´erence de [e-mail]://www.enseignement.polytechnique.fr/profs/informatique/Luc.Maranget/TLP/-2-A Typage implicite.B Inf´erence de type.C Unification.-3-Types implicitesIl est tr`es p´enible de devoir ´ecrireFun (x:Nat) -> x+1 Fun (x:Nat) -> Fun (y:Nat) -> x+yAlors que les types sont ici « ´evidents ». Si on ´ecritFun x -> x+1 Fun x -> Fun y -> x+yIl est clair que l’on peut facilement deviner que x et y doivent ˆetrede type Nat.On peut ensuite v´erifier le typage comme il y a quinze jours.-4-Typage implicite (`a la Curry)On pr´ef`ere deviner et v´erifier en mˆeme temps.Les r`egles,E⊕[x :A]⊢t :B E⊕[x :A]⊢t :AE ⊢ (Fun (x :A) -> t) :A -> B E ⊢ (Fix (x :A) -> t) :AdeviennentE⊕[x :A]⊢t :B E⊕[x :A]⊢t :AE ⊢ (Fun x -> t) :A -> B E ⊢ (Fix x -> t) :AEt c’est tout !-5-Pour ˆetre completVoici les autres r`egles qui ne changent pas.E(x) =A E ⊢t :Nat E ⊢t :Nat1 2E ⊢ n :NatE ⊢x :A E ⊢t op t :Nat1 2E ⊢t :Nat E ⊢t :A E ⊢t :A1 2 3E ⊢Ifz t Then t Else t :A1 2 3E ⊢t :A -> B E ⊢t :A1 2E ⊢t t :B1 2E ⊢t :A E⊕[x :A]⊢t :B1 2E ⊢Let x = t In t :B1 2En effet, il n’y a rien a` deviner ici (cf. le Let).6-6-Une vraie relationContrairement au typage explicite (a` la Church).On peut avoir E ⊢t :A et E ⊢t :A pour A =A .1 2 1 2Par ex.[x :Nat]⊢ x :Nat⊢ (Fun x -> x) :Nat -> NatEt[x :Nat -> Nat]⊢ x :Nat -> Nat⊢ (Fun x -> x) : (Nat -> Nat) -> Nat -> NatEt `a vrai dire, pour tout type A, on a facilement[x ...

Informations

• Publié par: Uctou
• Nombre de lectures: 16
• Langue: Français

Extrait

-1-

INF

554

Infe´rence

de

Luc Maranget

type

[e-mail] http://www.enseignement.polytechnique.fr/profs/ informatique/Luc.Maranget/TLP/

-2-

A

B

C

Typage

implicite.

Inf´erence

de

Unification.

type.

-3-

Types implicites

Ilesttre`spe´niblededevoire´crire

Fun(x:Nat) -> x+1Fun(x:Nat) ->Fun(y:Nat) -> x+y

Alors que les types sont ici«snt´edevi»io.S´nceirt

Funx -> x+1Funx ->Funy -> x+y

Il est clair que l’on peut facilement deviner quexetyodvietreentˆ de typeNat.

Onpeutensuiteve´rifierletypagecommeilyaquinzejours.

-4-

Typageimplicite(`alaCurry)

Onpr´ef`eredevineretve´rifierenmeˆmetemps.

Lesr`egles,

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

deviennent

E⊕[x:A]⊢t:B E⊢(Funx->t) :A->B

Et c’est tout !

E⊕[x:A]⊢t:A E⊢(Fix(x:A)->t) :A

E⊕[x:A]⊢t:A E⊢(Fixx->t) :A

-5-

P ˆtre complet our e

Voicilesautresre`glesquinechangentpas.

E(x) =A E⊢t 1 :NatE⊢t 2 :Nat E⊢n:Nat E⊢x:A E⊢t 1 opt 2 :Nat

E⊢t 1 :NatE⊢t 2 :A E⊢t 3 :A E⊢Ifzt 1 Thent 2 Elset 3 :A

E⊢t 1 :A->B E⊢t 2 :A E⊢t 1 t 2 :B

E⊢t 1 :A E⊕[x:A]⊢t 2 :B E⊢Letx=t 1 Int 2 :B

Eneffet,iln’yariena`devinerici(cf.leLet).

-6-

Une vraie relation

Contrairementautypageexplicite(`alaChurch).

On peut avoirE⊢t:A 1 etE⊢t:A 2 pourA 1 6=A 2 .

Par ex.

Et

[x:Nat]⊢x:Nat ⊢(Funx -> x) :Nat->Nat

[x:Nat->Nat]⊢x:Nat->Nat ⊢(Funx -> x) : (Nat->Nat)->Nat->Nat

Et`avraidire,pourtouttypeA, on a facilement

[x:A]⊢x:A ⊢(Funx -> x) :A->A

-7-

Exemple

Funx -> x+1est bien de typeNat->Nat.

[x:Nat]⊢x:Nat[x:Nat]⊢1:Nat

[x:Nat]⊢x+1:Nat

⊢(Funx -> x+1) :Nat->Nat

◮ehcnOonafrlpety`aherc.ntcoi

◮On devine le bon type pourx(Nat).

◮pyreOnche`aterchx+1.

◮On type les arguments de l’addition.

◮ire´vnOfiel’addition.

◮construit le type de la fonction.On

Maisilyaencoreunee´tapemagique:deviner[x:

Nat].

-8-

Variable de type

Funx -> x+1est de type ?X ->Nat, avec

Nat, avec [X=Nat].

[x:X]⊢x:X[x:X]⊢1:Nat

[x:X]⊢x+1:Nat[X=Nat]

⊢(Funx -> x+1) :X ->Nat[X=Nat]

◮no.alofcnite`atyperOncherch

◮On pose que le type dexestX

◮n.itio’addperlehcryta`Oehcn

◮Premier argument, second argument.

◮Pour typer d’addition il faut [X=Nat].

◮On type la fonction.

-9-

Id´eeg´en´eraledel’inference(synthe`se)detype ´

◮roPrea`´cdeasdinuserificev´en,enatio

⊲Introduisant des variables,

E⊕[x:X]⊢t:A

E⊢(Funx->t) :X->A

⊲edtnasoptEons.s´equati

E⊢t 1 :A 1 E⊢t 2 :A 2 E⊢t 1 +t 2 :Nat[A 1 =Nat A 2 =Nat]

` ◮nfialano,Aoitauqe´.snriabesvatdesleseepocnuytnadttnne

-10-

Retoursurlav´erification

Lestypessontdoncchang´es,ilspeuventcontenirdesvariables.

Nat∈ T

X∈ T

Avec les nouveaux types on a :

[x:X]⊢x:X

A 1 ∈ TA 2 ∈ T A 1 ->A 2 ∈ T

⊢(Funx -> x) :X -> X

Quelsensdonner`aunteltype?

id:X -> Xveut dire queid:A->Apour tout typeA.

Eteneffetonpeutdonnerlestypessuivants`aFunx -> x.

◮Nat->Nat, (Nat->Nat)->Nat->Nat, etc.

◮Et meme (Y -> Z)-> Y -> Z, mais pasY ->Nat. ˆ

Etˆeme(Y -> Z)-> Y -> Z, mais pasY -> ◮m

-11-

S´emantique:

Variables dans les types

SiXatıˆarappnsdaA, type det, alors [X7→B]Aest aussi un type detpour tout typeB.

Note :[X7→B] est une nouvelle notation pour la substitution, cettefoisapplique´eauxtypes.

Rappels/Remarques.

◮Substitution : fonction des variables dans les termes.

◮esrmteux:´,tnemelaeudneteicaFσ(A->B) =σ(A)->σ(B).

◮Substitutions de support fini{X|σ(X)6=X}.

◮Pdeasobpreml`seedactpruieic.