Polynomial Size Analysis of First-Order Shapely Functions

We present a size-aware type system for first-order shapely functiondefinitions. Here, a function definition is called shapely when the size of theresult is determined exactly by a polynomial in the sizes of the arguments.Examples of shapely function definitions may be implementations of matrixmultiplication and the Cartesian product of two lists. The type system isproved to be sound w.r.t. the operational semantics of the language. The typechecking problem is shown to be undecidable in general. We define a naturalsyntactic restriction such that the type checking becomes decidable, eventhough size polynomials are not necessarily linear or monotonic. Furthermore,we have shown that the type-inference problem is at least semi-decidable (underthis restriction). We have implemented a procedure that combines run-timetesting and type-checking to automatically obtain size dependencies. Itterminates on total typable function definitions.Comment: 35 pages, 1 figur