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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Matrix Coeffect Algebra for Interdependent Context Requirements

  • Osamu Miyazawa,
  • Shin-ya Nishizaki

摘要

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.