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

TL;DR

This paper introduces mor^{na}, a non-affine dependent type system that improves resource analysis of higher-order functional programs by decoupling resource reasoning from types, enabling more precise bounds.

Contribution

It proposes mor^{na}, a novel non-affine, dependent type system that enhances resource analysis accuracy for higher-order programs by separating resource annotations from types.

Findings

Formalized syntax and semantics of mor^{na}

Proved soundness of the type system

Demonstrated expressiveness with complex examples

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_\ms{amor}^\ms{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_\ms{amor}^\ms{na}} decouples resources from types and follows a non-affine typing mechanism. The non-affine type system of \lambda_\ms{amor}^\ms{na}} achieves this by using dependent types, which allows expressing type-level potential functions separate from ordinary types. This article formalizes \lambda_\ms{amor}^\ms{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_\ms{amor}^\ms{na}}'s reasoning capability.