Re: Algorithme de Milner (synth=?iso-8859-1?Q?�?= se de type)

[Didier.Remy@inria.fr (Didier Remy)]

> Quelqu'un connaîtrait-il une page Web décrivant le principe de l'algorithme
> H-M pour la synthèse de type à la ML ? C'est pour donner une réf. à un
> étudiant 
> qui doit le réaliser.

En annexe de [1], j'ai décrit une implémentation de l'algorithme de Milner, 
et le code Caml-Light correspondant.

Les types sont représentés par des graphes plutôt que des termes afin de
profiter au maximum du partage naturellement crée par l'unification. De plus
ce partage est conservé au cours des opérations de généralisation et
d'instantiation.

L'algorithme résultant a la même complexité que la borne théorique (ce qui
n'est pas le cas des algorithmes habituellement implantés), et se comporte
également très bien en pratique.

La contrepartie est que l'implémentation est un peu alourdie par
l'utilisation de graphes.

        --Didier


[1] @TechReport{Remy!mleth,
author     = "Didier R{\'e}my",
title      = "Extending {ML} Type System with a Sorted
              Equational Theory", 
institution= "Institut National de Recherche en Informatique et Automatisme",
address    = "Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France",
type       = "Research Report",
number     = 1766,
year       = 1992
}