cours sur le polymorphisme

-1-INF 554 Luc MarangetPolymorphismeLuc.Maranget@inria.frhttp://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 ...