Vector Graphics through Category Theory
摘要
This paper introduces a novel approach to vector graphics drawing by formalizing it within Category Theory (CT). Using the categorical programming paradigm, CT abstractions are interpreted as design patterns within Functional Programming (FP), bridging theoretical formalism and practical implementation. Building on Yorgey’s work, we represent diagrams as lists of graphical primitives, serving as a normal form for vector graphics. Diagrams are manipulated via graphical transformations (e.g., translation, rotation, scaling, color change) and list concatenation, which are modeled as an endofunctor F. This enables the construction of a free monad \(\mathbb {T} \cong \texttt {Free F}\) as a way to accumulate operations into expression trees lazily. We formalize graphical marks as abstractions over diagrams via slice categories, and vector graphics as values of the free monad \(\mathbb {T}\) over marks. Lastly, we introduce graphic expressions as a way to leverage F-algebras and F-coalgebras to construct complex graphics systematically. A prototype implementation in Lean demonstrates the applicability of our theory in a programming language based on dependent types, illustrating how categorical programming bridges the gap between mathematical abstraction and practical programming. An implementation in Julia is presented elsewhere.