Thursday, 14 August 2008, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
Slides from the talk [pdf]
Abstract: Recently we have presented a size-aware type system for first-order shapely function definitions. A function definition is called shapely when the size of the result is determined exactly by a polynomial in the sizes of the arguments.
At present we study generalisation of the method to function definitions with size dependencies limited by (piecewise) polynomials from above and below. A simple example of such definition is an encoding of insertion an element into a list.
The main idea is to annotate an output type not with a single polynomial, but with a parametrised family of (piecewise) polynomials, where a parameter(s) varies inside a certain range. Type-checking amounts to instantiation of the parameter of the type under checking. It must force equality of two polynomials and belong to the range.
This problem is undecidable in non-linear integer arithmetic, so one has to involve real arithmetic. We have designed a form of type annotations which significantly simplifies predicates arising at the end of type-checking.
Similarly to shapely function definitions, one may involve testing to infer lower and upper bounds, once these bounds are polynomials. The condition is that for (almost) any vector of input sizes there are inputs on which the minimal output size is achieved and inputs on which the maximal size is achieved.
To extend applicability, we allow higher-order functions, if an output annotation does not depend on size parameters/dependencies of the non-zero-order arguments. Thus we cover almost all function definitions, say, from the Clean lists library. (Joint work with M. van Eekelen, A. Tamalet.)