Nous nous intéressons à une extension de ML avec polymorphisme<br />de première classe, à la manière du Système F.<br />Cette extension, nommée MLF, utilise les annotations de types<br />d'ordre supérieur données explicitement dans le programme pour inférer<br />de manière principale le type le plus général. Toute expression admet<br />ainsi un type principal, qui dépend des annotations présentes<br />initialement dans le programme.<br /><br />Toute expression de ML est typable dans MLF sans annotation<br />supplémentaire. Les expressions du Système F sont encodées de<br />manière systématique dans MLF en supprimant les abstractions<br />et les applications de types, et en traduisant les annotations<br />de types dans le langage de types de MLF.<br />De plus, les paramètres de lambda-abstractions qui ne sont pas<br />utilisés de manière polymorphe n'ont pas besoin d'être annotés.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00007132 |
| Date | 06 May 2004 |
| Creators | Le Botlan, Didier |
| Publisher | Ecole Polytechnique X |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | English |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0022 seconds