Algorithme de Milner (synthè se de type)

Algorithme de Milner (synthè se de type)

[Jean Charles Gregoire]

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.


Merci


Would anyone know of an online ref for the H-M algorithm for type synthesis?
I would like to have this for a student who must implement it.

Thanks,

J-Ch. Grégoire.

Re: Algorithme de Milner (synthè se de type)

[Fredrik Granlund]

On Wed, 12 Nov 1997, Jean Charles Gregoire wrote:

>
> 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.
>
> Merci
>
> Would anyone know of an online ref for the H-M algorithm for type
> synthesis? I would like to have this for a student who must implement
> it. Thanks,  J-Ch. Grégoire.

I suggest you have a look at Luca Cardellis homepage. He has written a
paper entitled "Basic Polymorphic Typechecking" as well as a lot of other
papers on types and type systems. They are all available online.

http://www.luca.demon.co.uk/Papers.html

Hope this helps.


///Fredrik

--
Fredrik Granlund                              | Phone:  +46 31 747 00 00
Ericsson Microwave Systems AB                 | Direct: +46 31 747 00 42
Airborne Radar Division                       | Home:   +46 31 776 57 64
Software Engineering Environments             | Fax:    +46 31 747 31 08
Bergfotsgatan 2, S-431 84  MÖLNDAL, SWEDEN
E-mail: Fredrik.Granlund@emw.ericsson.se

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

[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
}