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

2021/01/23 by Mu, Shin-Cheng
#FOS: Computer and information sciences #Programming Languages (cs.PL)

paper · doi:10.48550/arxiv.2101.09408

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.

Related

• Combining nondeterminism, probability, and termination: equational and metric reasoning
• Calculating a backtracking algorithm: an exercise in monadic program derivation
• Equational Reasoning for MTL Type Classes
• Effects Without Monads: Non-determinism -- Back to the Meta Language
• Effectful Programming in Declarative Languages with an Emphasis on Non-Determinism: Applications and Formal Reasoning