cours sur le polymorphisme

Description

-1-INF 554 Luc [e-mail]://www.enseignement.polytechnique.fr/profs/informatique/Luc.Maranget/TLP/-2-A Polymorphisme.B Inf´erence des types polymorphes.-3-Limitation des types simplesL’identit´e Fun x -> x a plusieurs types.Type principal X -> X.Mais Let id = Fun x -> x In id id n’est pas typable.[id : X -> X]⊢ id; X -> X, ∅ [id : X -> X]⊢ id; X -> X, ∅[id : X -> X]⊢ id id; Y, (X -> X) = ((X -> X) -> Y)Ce qui conduit finalement a` l’´equation X = X -> X, qui n’a pas desolution.Et pourtant, puisque id poss`ede tous les types A -> A, les typessuivants sont possibles pour la premi`ere et la seconde occurrencede id.(Z -> Z) -> (Z -> Z) Z -> ZEt l’application id id a pour type Z -> Z.-4-SolutionAutoriser des instances diff´erentes σ(A) d’un mˆeme type.Enrichir les types :A ∈T A ∈T A∈T1 2Nat∈T X ∈TA -> A ∈T ∀X[A]∈T1 2Ajouter une r`egle « d’´elimination » de ∀.E ⊢t :∀X[A]E ⊢t :A[X 7!B]On parle aussi d’instanciation (de la variable li´ee X).(Il nous faut aussi une r`egle « d’introduction » de ∀, mais laissonscela de coˆt´e pour le moment).-5-En passant...Les types contienent maintenant un lieur (∀), comme les termes(Fun etc.)Ceci complique la d´efinition de la substitution qui doit ´eviter lescaptures des variables libres.F(X) ={X} F(Nat) =∅ F(A -> B) =F(A)∪F(B)F(∀X[A]) =F(A)\{X}Et pour la substitution(∀X[A])[X 7!B] =∀X[A](∀X[A])[Y 7!B] =∀X[A[Y 7!B]] avec X 62F(B) (Gros bug !)-6-Identitit´e ...

Informations

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

Extrait

-1-

INF

554

Luc Maranget

Polymorphisme

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

-2-

A

B

Polymorphisme.

Inf´erence

des

typ

es

p

olymorphes.

-3-

Limitation des types simples

L’identite´Funx -> xa plusieurs types.

Type principalX -> X.

MaisLetid=Funx->xInid idn’est pas typable.

[id:X -> X]⊢id❀X -> X∅[id:X -> X]⊢id❀X -> X∅ [id:X -> X]⊢id id❀Y(X -> X) = ((X -> X) -> Y)

Cequiconduitfinalementa`l’e´quationX=X -> X, qui n’a pas de solution.

Et pourtant, puisqueidde`esspostleustosepyA->A, les types suivantssontpossiblespourlapremie`reetlasecondeoccurrence deid.

(Z -> Z) -> (Z -> Z)

Et l’applicationid ida pour typeZ -> Z.

Z -> Z

-4-

Solution

Autoriserdesinstancesdiff´erentesσ(Ametype.)d’unmˆe

Enrichir les types :

N t∈ TX∈ T A 1 ∈ TA 2 ∈ T a A 1 ->A 2 ∈ T

Ajouterunere`gle«atioimin’´eldn»de∀.

E⊢t:∀X[A] E⊢t:A[X7→B]

A∈ T ∀X[A]∈ T

On parle aussitaoinicnatsni’d(edalavirbaleli´eeX).

(Ilnousfautaussiunere`gle«noind’odtrtiuc»de∀, mais laissons celadecˆot´epourlemoment).

-5-

En passant. . .

Les types contienent maintenant un lieur (∀), comme les termes (Funetc.)

Cecicompliquelade´finitiondelasubstitutionquidoit´eviterles captures des variables libres.

F(X) ={X} F(Nat) =∅ F(A->B) =F(A)∪ F(B)

F(∀X[A]) =F(A) {X}

Et pour la substitution

(∀X[A])[X7→B] =∀X[A]

(∀X[A])[Y7→B] =∀X[A[Y7→B]]avecX6∈ F(B) (Gros bug !)

-6-

Identitite´polymorphe

Dans l’environnementE=id:∀X[X -> X], on souhaite typer l’applicationid id.

On y arrive par exemple ainsi.

E⊢id:∀X[X -> X]

E⊢id:∀X[X -> X]

E⊢id:-> Z) -> (Z -> Z)(Z E⊢id:Z -> Z

E⊢(id id) :Z -> Z

Les deux occurrences deiddneonlint`aeuxuednstsniicnaoita diff´erentes.

◮-> Z) -> (Z -> Z)(Z = (X -> X)[X7→(Z -> Z)]

◮Z -> Z= (X -> X)[X7→Z]

-7-

Int´erˆetdupolymorphisme

◮ursiopenofeuu,`hqeadsnnusnbibetoilfin´edeironsfioctD toutes.

◮Les utiliser avec des types divers.

Exemple : composition de fonctions.

◮D´efinir: l e t(>>>)f g=funx->f(g x) comp : (’a -> ’b) -> (’c -> ’a) -> ’c -> ’b

◮Emploi : l e tf= string_of_int>>> (funx->x+2) >>>int_of_string f : string -> string

f"5" - : string = "7"

-8-

Structuresdedonn´eespolymorphes

La liste deX(nepye´toesnttu∀’a.)’a listpira´efinml.DenCa deux«tsurcnorseuct»

◮Nil ([]), de type (∀’a.)’a list.

◮Cons (::), de type (∀’a.)’a-> ’a list-> ’a list.

Toutes les fonctions qui ne«regardent pas»directement les ´ele´ments(detype’a) sont polymorphes. l e t rec f y0 xsfold right=matchxswith _ | [] ->y0 |x::xs->f x(fold_right f y0 xs) fold_right : (’a -> ’b -> ’b) -> ’b -> ’a list -> ’b

Calculef(x 1  f(x 2  . . . f(x n  y 0 ))). Ou (plus classique) un tri : sort : ’a list -> (’a -> ’a -> bool) -> ’a list

-9-

Int´erˆetthe´oriquedupolymorphisme

Des constructions classiques duλat`r´CFuiedluP(accl-Fun, application et variables) sont typables.

Par exemple, l’encodage suivant des entiers, montre que nos constantesetop´erateurssurlesentierssontinutiles(dumoinsen the´orie).

◮Les entiers (dits de Church) Letzero=Funf->Funx->x Letun=Funf->Funx->f x . . .

L’entiernest le terme

Funf ->Funx -> f(f  (f x)) { } noitacilpapsn

◮Le type des entiers estN=∀X[(X -> X) -> X -> X].

-10-

Type des entiersN=∀X[(X -> X) -> X -> X]

Certaines primitives (toutes ?) sur les entiers sont alors typables:

◮uSccseesur Letsucc=Funn->Funf->Funx->n f(f x)

TypeN -> N.

◮Addition et multiplication.

Letadd= Funn1->Funn2-> Funf->Funx->n1 f(n2 f x) Letmul= Funn1->Funn2-> Funf->Funx->n1(n2 f)x

De typesN -> N -> N.

-11-

Introduction du∀

Revenons sur le typage desucc

N=∀X[(X -> X) -> X -> X]

E⊢n:N

Z -> Z)-

E⊢n: (Z -> Z)-> Z -> ZE⊢f:Z -> Z

E⊢(n f) :Z -> Z

[n:N;f:Z -> Z;x:Z]⊢n f (f x):Z

.

E⊢(f x) :Z

[n:N;f:Z -> Z]⊢(Fun f (f x)x -> n) :Z -> Z

[n:N]⊢(Funf ->Funx -> n f (f x)) :(Z -> Z) -> Z -> Z

On veut conclure

[n:N]⊢(Funf ->Funx ->  ) :∀Z[(Z -> Z) -> Z -> Z]

Et donc (variable muette),succde typeN->N.