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