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

翻译：静态资源分析无需执行程序即可确定其资源消耗（例如时间复杂度）。在现有的众多资源分析方法中，仿射类型系统一直是主流方法之一。然而，这些仿射类型系统难以推导高阶程序的精确资源行为，尤其是在涉及部分应用的情况下。本文提出λ_\ms{amor}^\ms{na}}，一种用于高阶函数式程序资源推理的非仿射AARA风格依赖类型系统。关键观察在于：先前方法的主要问题源于（i）类型与资源的紧密耦合，以及（ii）仿射类型机制与高阶类型机制之间的冲突。为推导高阶函数的精确资源行为，λ_\ms{amor}^\ms{na}}将资源与类型解耦，并采用非仿射类型机制。该非仿射类型系统通过使用依赖类型实现这一目标，使得类型级势函数能够独立于普通类型进行表达。本文形式化了λ_\ms{amor}^\ms{na}}的语法与语义，并证明其可靠性——这保证了资源界限的正确性。文中通过若干具有挑战性的经典高阶示例，展示了λ_\ms{amor}^\ms{na}}推理能力的表达性与组合性。