Effectful Aggregate Computation: towards a monadic view

Aggregate computing is a macro-programming paradigm for distributed systems in which a single global program describes the behavior of an entire collective of devices. Rather than focusing on explicit message passing or device-level coordination, programs specify collective behavior that emerges from local execution and neighbour interaction. Core coordination mechanisms, such as alignment, enable this global perspective by structuring how devices combine local and neighbouring information. Because these mechanisms influence program evaluation in ways that are not explicitly reflected in the syntax, they can be understood as computational effects. This thesis introduces a monadic formulation of aggregate computation, modeling aggregation as a first-class effect. This reformulation restores key properties of purely functional programming, such as equational reasoning and disciplined composition, while encapsulating the semantics of aggregate computing into a principled, language-agnostic abstraction. A Scala implementation is presented, encoding the constructs of the eXchange Calculus as a monadic API. The design enforces a clear boundary between pure and aggregate computations at the type level, thereby simplifying reasoning, improving testability, and enabling safe refactoring. Alongside the implementation, proof sketches are provided to show that the implementation satisfies the monad laws. The resulting framework has the potential to unify aggregate computing with well-established theories of effects, providing a principled foundation for structuring and reasoning about distributed programs.