Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures

Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures
Nils Anders Danielsson
Conference record of the 35th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL 2008). © ACM, 2008. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in POPL'08, http://doi.acm.org/10.1145/1328438.1328457. Accompanying technical report. [pdf, accompanying code]

Abstract

Okasaki and others have demonstrated how purely functional data structures that are efficient even in the presence of persistence can be constructed. To achieve good time bounds essential use is often made of laziness. The associated complexity analysis is frequently subtle, requiring careful attention to detail, and hence formalising it is valuable.

This paper describes a simple library which can be used to make the analysis of a class of purely functional data structures and algorithms almost fully formal. The basic idea is to use the type system to annotate every function with the time required to compute its result. An annotated monad is used to combine time complexity annotations.

The library has been used to analyse some existing data structures, for instance the deque operations of Hinze and Paterson's finger trees.

Erratum

In the typing rule for fix (in Section 10) the term fix t should be replaced by fix (λx.t).