Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
pspdfbibcode(advi slides of appsem04 talk)(advi slides of icfp04 talk, more detailed)
Numbering Matters: First Order Canonical Forms for Second-Order Recursive Types.
Nadji Gauthier and François Pottier.
Submitted to ICFP'04, April 2004.
Abstract : We study a type system equipped with universal types and equirecursive types,
which we refer to as \fmu. We show that type equality may be decided in time
$O(n\log n)$, an improvement over the previous known bound of $O(n^2)$. In
fact, we show that two more general problems, namely entailment of type
equations and type unification, may be decided in time $O(n\log n)$, a new
result. To achieve this bound, we associate, with every \fmu type, a
\emph{first-order canonical form}, which may be computed in time $O(n\log n)$.
By exploiting this notion, we reduce all three problems to equality and
unification of \emph{first-order} recursive terms, for which efficient
algorithms are known.
ps.gzpdf(advi slides)
Rapport de Dea Programmation, "Défonctionalisation Typée Polymorphe"
Abstract :
La défonctionalisation est une transformation de programme qui vise à
changer un programme fonctionnel d'ordre supérieur en un du premier ordre, c'est à dire
à éliminer l'emploi de fonction comme valeurs de première classe. Son but est donc identique à
celui de la conversion en clôture. Mais elle se distingue par le fait
qu'elle stocke un tag, au lieu d'un pointeur de code, à l'intérieur des clôtures.
La défonctionalisation a été utilisée à la fois comme un outil de raisonnement et
comme technique de compilation.
La défonctionalisation est d'habitude définie et étudiée dans le cadre du lambda calcul
simplement typé, où il est prouvé que la sémantique et le typage sont préservés. On a
observé que dans le cadre d'un système de type polymorphe, comme celui de ML ou de Système F,
que la défonctionalisation ne préserve pas le typage. Dans ce rapport nous montrons qu'en étendant
Système F avec des types algébriques gardés, nous parvenons à retrouver la préservation
du typage. Ce résultat permet d'ajouter la défonctionalisation à l'ensemble des techniques
de compilation typée.
Néanmoins cette formalisation ne se prête pas directement à une implémentation du vérificateur de type
principalement à cause de la
présence de la règle de sous-typage dans le système de type présenté. Il est donc nécessaire
de modifier le système pour le rendre dirigé par la syntaxe. On montre également que des versions non naïves
de la défonctionalisation existent, et donnent des résulats intéressants, ce qui permet d'exploiter cette transformation comme
technique optimisante de compilation typée.
@INPROCEEDINGS{gauthier-pottier-04,
AUTHOR = {Nadji Gauthier and François Pottier},
TITLE = {Numbering Matters: First-Order Canonical Forms for Second-Order Recursive Types},
BOOKTITLE = {Proceedings of the 2004 {ACM} {SIGPLAN} International
Conference on Functional Programming (ICFP'04)},
URL = {http://pauillac.inria.fr/~fpottier/publis/gauthier-fpottier-icfp04.ps.gz},
PDF = {http://pauillac.inria.fr/~fpottier/publis/gauthier-fpottier-icfp04.pdf},
ACM = {http://doi.acm.org/10.1145/1016850.1016872},
MONTH = SEP,
YEAR = {2004},
PAGES = {150--161},
ABSTRACT = {We study a type system equipped with universal types and equirecursive types,
which we refer to as $F_\mu$. We show that type equality may be decided in time
$O(n\log n)$, an improvement over the previous known bound of $O(n^2)$. In
fact, we show that two more general problems, namely entailment of type
equations and type unification, may be decided in time $O(n\log n)$, a new
result. To achieve this bound, we associate, with every $F_\mu$ type, a
\emph{first-order canonical form}, which may be computed in time $O(n\log n)$.
By exploiting this notion, we reduce all three problems to equality and
unification of \emph{first-order} recursive terms, for which efficient
algorithms are known.}
}