Dynamic features in array programming languages’ type systems are based on runtime assertions, compiler specialization, and existential quantification. Even approaches using dependent types resolve data-dependent shapes (array sizes determined by computations on data) via these mechanisms. In this work, we address static rank polymorphism using recursion morphisms and F-algebras, making folds the core computational mechanism. We show that \textit{graded monoids} are indexing algebras of such folds, and can be used to unify shape resolution approaches.

Specifically, in an array language where all operations are folds, folding permits computation of both the value and index metadata in a single pass. Algebra homomorphisms certify the coherence of such operations and classify them by shape effect; shape-preserving, -shrinking, or -growing. In the context of graded monoids, a single per-step proof obligation that the index evolves independently of the fiber suffices to show well-formedness; the monoid homomorphism lifts it to an algebra homomorphism. The index metadata collected by the monoid enables functions to build results having dependent types and has applications beyond typing.