Matrix Coeffect Algebra for Interdependent Context Requirements
摘要
Coeffects capture requirements that the environment imposes on programs. Petricek’s structural coeffect calculus extends the simply typed lambda calculus with a type-and-coeffect system. In this framework, requirements such as variable reuse counts and the number of past values needed in dataflow languages are represented by scalars drawn from algebraic structures that relax some semiring axioms (coeffect algebras). However, existing scalar- and vector-based coeffect domains combine annotations componentwise and therefore do not naturally capture constraints between interacting contextual quantities, such as travel times between airports and departure times at airports. To address this limitation, we introduce Matrix Coeffect Algebra, a matrix-valued coeffect domain whose composition propagates requirements across contextual components, enabling constraints between interdependent quantities. We embed Matrix Coeffect Algebra into Petricek’s structural coeffect calculus and prove its type safety via his translational semantics. A flight-timetable case study demonstrates that matrix-based coeffects enable dependency-aware static checking in a coeffect type system. Our technical contribution is a new matrix-valued coeffect algebra, used as an instantiation of Petricek’s structural (schematic) coeffect calculus.