Stratified type inference for generalized algebraic data types

Abstract : We offer a solution to the type inference problem for an extension of Hindley and Milner's type system with generalized algebraic data types. Our approach is in two strata. The bottom stratum is a core language that marries type inference in the style of Hindley and Milner with type checking for generalized algebraic data types. This results in an extremely simple specification, where case constructs must carry an explicit type annotation and type conversions must be made explicit. The top stratum consists of (two variants of) an independent shape inference algorithm. This algorithm accepts a source term that contains some explicit type information, propagates this information in a local, predictable way, and produces a new source term that carries more explicit type information. It can be viewed as a preprocessor that helps produce some of the type annotations required by the bottom stratum. It is proven sound in the sense that it never inserts annotations that could contradict the type derivation that the programmer has in mind.
Type de document :
Communication dans un congrès
POPL'06 - Proceedings of the 33rd ACM Symposium on Principles of Programming Languages, Jan 2006, Charleston, South Carolina, United States. pp.232--244, 2006, 〈http://dl.acm.org/citation.cfm?id=1111037.1111058&coll=DL&dl=ACM&CFID=56655396&CFTOKEN=73618070〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00629091
Contributeur : Yann Regis-Gianas <>
Soumis le : mercredi 5 octobre 2011 - 08:47:23
Dernière modification le : vendredi 25 mai 2018 - 12:02:03

Identifiants

  • HAL Id : inria-00629091, version 1

Collections

PPS | INRIA | USPC

Citation

François Pottier, Yann Régis-Gianas. Stratified type inference for generalized algebraic data types. POPL'06 - Proceedings of the 33rd ACM Symposium on Principles of Programming Languages, Jan 2006, Charleston, South Carolina, United States. pp.232--244, 2006, 〈http://dl.acm.org/citation.cfm?id=1111037.1111058&coll=DL&dl=ACM&CFID=56655396&CFTOKEN=73618070〉. 〈inria-00629091〉

Partager

Métriques

Consultations de la notice

113