Message-Id: <199711190849.JAA05558@pauillac.inria.fr>
Subject: Re: Algorithme de Milner =?us-ascii?Q?=28synth==3Fiso=2D8859=2D1=3FQ=3F=E8=3F=?= se de type)
In-Reply-To: <323_8540_879362618_1@someware> from Jean Charles Gregoire at "Nov 12, 97 02:23:39 pm"
To: gregoire@inrs-telecom.uquebec.ca (Jean Charles Gregoire)
Date: Wed, 19 Nov 1997 09:49:01 +0100 (MET)
From: 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
}
This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:12 MET