Equational reasoning for non-determinism monad: the case of Spark aggregation

TL;DR

This paper explores equational reasoning techniques for the non-determinism monad, specifically applied to Spark aggregation, by identifying key properties, introducing helpful operators, and proving relevant properties.

Contribution

It introduces new operators and notations for equational reasoning about non-determinism monads and demonstrates their effectiveness through proofs related to Spark aggregation.

Findings

Identified key properties for non-determinism monad

Developed operators to facilitate reasoning

Proved properties in Spark aggregation context

Abstract

As part of the author's studies on equational reasoning for monadic programs, this report focus on non-determinism monad. We discuss what properties this monad should satisfy, what additional operators and notations can be introduced to facilitate equational reasoning about non-determinism, and put them to the test by proving a number of properties in our example problem inspired by the author's previous work on proving properties of Spark aggregation.