Dependently-Typed AARA: A Non-Affine Approach for Resource Analysis of Higher-Order Programs

Abstract

Static resource analysis determines the resource consumption (e.g., time complexity) of a program without executing it. Among the numerous existing approaches for resource analysis, affine type systems have been one dominant approach. However, these affine type systems fall short of deriving precise resource behavior of higher-order programs, particularly in cases that involve partial applications.

This article presents $\lambda_{\mathsf{amor}}^{\mathsf{na}}$, a non-affine AARA-style dependent type system for resource reasoning about higher-order functional programs. The key observation is that the main issue in previous approaches comes from (i) the close coupling of types and resources, and (ii) the conflict between affine and higher-order typing mechanisms. To derive precise resource behavior of higher-order functions, $\lambda_{\mathsf{amor}}^{\mathsf{na}}$ decouples resources from types and follows a non-affine typing mechanism. The non-affine type system of $\lambda_{\mathsf{amor}}^{\mathsf{na}}$ achieves this by using dependent types, which allow expressing type-level potential functions separate from ordinary types. This article formalizes $\lambda_{\mathsf{amor}}^{\mathsf{na}}$’s syntax and semantics, and proves its soundness, which guarantees the correctness of resource bounds. Several challenging classic and higher-order examples are presented to demonstrate the expressiveness and compositionality of $\lambda_{\mathsf{amor}}^{\mathsf{na}}$’s reasoning capability. This article also includes an algorithmic variant of $\lambda_{\mathsf{amor}}^{\mathsf{na}}$’s type system and a discussion of the automation of type checking and inference for $\lambda_{\mathsf{amor}}^{\mathsf{na}}$.