Polymorphic Types with Polynomial Sizes
1 : ANSYS
Ansys inc.
2 : Inria Paris-Rocquencourt
Institut National de Recherche en Informatique et en Automatique
INRIA Rocquencourt : Domaine de Voluceau, Rocquencourt B.P. 105 78153 le Chesnay Cedex -
France
3 : Ecole normale supérieure – PSL (Paris)
* : Auteur correspondant
L'Institut National de Recherche en Informatique et e n Automatique (INRIA)
We present a compile-time analysis for tracking the size of data-structures in a statically typed and strict functional language. This information is valuable for static checking and code generation. Rather than relying on dependent types, we propose a type-system close to that of ML: polymorphism is used to define functions that are generic in types and sizes; both can be inferred. This approach is convenient, in particular for a language used to program critical embedded systems, where sizes are indeed known at compile-time. By using sizes that are multivariate polynomials, we obtain a good compromise between the expressiveness of the size language and its properties (verification, inference).