---
abstract: 'This paper introduces a new methodology for the complexity analysis of higher-order functional programs, which is based on three components: a powerful type system for size analysis and a sound type inference procedure for it, a ticking monadic transformation and a concrete tool for constraint solving. Noticeably, the presented methodology can be fully automated, and is able to analyse a series of examples which cannot be handled by most competitor methodologies. This is possible due to various key ingredients, and in particular an abstract index language and index polymorphism at higher ranks. A prototype implementation is available.'
author:
- Martin Avanzini
- Ugo Dal Lago
bibliography:
- 'references.bib'
title: |
    Automating Sized-Type Inference\
    and Complexity Analysis
---

Introduction
============

One successful approach to automatic verification of termination properties of higher-order functional programs is based on *sized types* [@HPS:POPL:96]. In sized types, a type carries not only some information about the *kind* of each object, but also about its *size*, hence the name. This information is then exploited when requiring that recursive calls are done on arguments of *strictly smaller* size. Estimating the size of intermediate results is crucial for complexity analysis, but up to now, the only attempt of using sized types for complexity analysis is due to Vasconcelos [@Vasconcelos:Diss:08], and confined to space complexity. If one wants to be sound for time analysis, size types need to be further refined, e.g., by turning them into linear dependently types [@LG:LMCS:11]. Since the first inception in the seminal paper of Hughes et. al. [@HPS:POPL:96] the literature on sized typed has grown to a considerable extend. Indeed, various significantly more expressive systems have been introduced, with the main aim to improve the expressiveness in the context of termination analysis. For instance, Blanqui [@Blanqui:CSL:05] introduced a novel sized type system on top of the *calculus of algebraic construction*. Notably, it has been shown that for size indices over the successor algebra, type checking is decidable [@Blanqui:CSL:05]. The system is thus capable of expressing additive relations between sizes. In the context of termination analysis, where one would like to statically detect that a recursion parameter decreases in size, this is sufficient. In this line of research falls also more recent work of Abel and Pientka [@AP:JFP:16], where a novel sized type system for termination analysis on top of $\mathsf{F}_\omega$ is proposed. Noteworthy, this system has been integrated in the dependently typed language .[^1] As we will see, capturing only additive relations between value sizes is not enough for our purpose. On the other hand, even slight extensions to the size index language render current methods for type inference, even type checking, intractable. In this paper, we thus take a fresh look at sized-type systems, with a particular emphasis on a richer index language and feasible automation on existing constraint solving technology. Our system exhibits many similarities with the archetypal system from [@HPS:POPL:96], which itself is based on a Hindley-Milner style system. Although conceptually simple, our system is substantially more expressive than the traditional one. This is possible mainly due to the addition of one ingredient, viz, the presence of *arbitrary rank index polymorphism*. That is, functions that take functions as their argument can be polymorphic in their size annotation. Of course, our sized type system is proven a sound methodology for *size* analysis. In contrast to existing works, one can also device an inference machinery that is sound and (relative) complete. Finally, this system system is amenable to time complexity analysis by a ticking monadic transformation. A prototype implementation is available, see below for more details. More specifically, our contributions can be summarized as follows:

We show that size types can be generalised so as to encompass a notion of index polymorphism, in which (higher-order subtypes of) the underlying type can be universally quantified. This allows for a more flexible treatment of higher-order functions. Noticeably, this is shown to preserve soundness (i.e. subject reduction), the minimal property one expects from such a type system. On the one hand, this is enough to be sure that types reflect the size of the underlying program. On the other hand, termination is not enforced anymore by the type system, contrarily to, e.g. [@Blanqui:CSL:05; @AP:JFP:16]. In particular, we do not require that recursive calls are made on arguments of smaller size.

The polymorphic sized types system, by itself, does not guarantee any complexity-theoretic property on the typed program, except for the *size* of the output being bounded by a function on the size of the input, itself readable from the type. Complexity analysis of a program $\progone$ can however be seen as a size analysis of another program $\tprogone$ which computes not only $\progone$, but its complexity. This transformation, called the *ticking transformation*, has already been studied in similar settings [@DLR:ICFP:15].

Contrarily to many papers from the literature, we have taken care not only of constraint *inference*, but also of constraint *solving*. This has been done by building a prototype called which implements type inference and ticking, and then relies on an external tool, called , to check the generated constraints for satisfiability. borrows heavily from the advances made over the last decade in the synthesis of *polynomial interpretations*, a form of polynomial ranking function, by the rewriting community. It features also some novel aspects, most importantly, a bottom-up SCC analysis for incremental constraint solving. We thus arrive at a fully automated runtime analysis of higher-order functional programs. Noteworthy, we are able to effectively infer polynomial, not necessarily linear, bounds on the runtime of programs.

Both tools are open source and available from the first authors homepage. [^2]  is able to analyse, fully automatically, a series of examples which cannot be handled by most competitor methodologies. Indeed, it is to our best knowledge up until today the only approach that can fully deal with function closures whose complexity depends on the captured environment, compare for instance the very recent work of Hoffmann et. al. [@HDW:POPL:17]. Dealing with such closures is of crucial importance, e.g., when passing partially applied functions to higher-order combinators, a feature pervasively used in functional programming.

For brevity, we only give a formalisation of our system and state the central theorem here. An extended version, including all the technical details is available online [@EV].

Our Type System at a Glance {#sect:ERW}
===========================

Applicative Programs and Simple Types {#sect:APST}
=====================================

Sized Types and Their Soundness {#sect:STS}
===============================

Conclusions {#sect:C}
===========

[^1]: See <http://wiki.portal.chalmers.se/agda>.

[^2]: See <https://cl-informatik.uibk.ac.at/users/zini/software>.
