paper

Preservation of Equations by Monoidal Monads

arXiv:2001.06348

Abstract

If a monad is monoidal, then operations on a set can be lifted canonically to operations on . In this paper we study structural properties under which preserves equations between those operations. It has already been shown that any monoidal monad preserves linear equations; affine monads preserve drop equations (where some variable appears only on one side, such as ) and relevant monads preserve dup equations (where some variable is duplicated, such as ). We start the paper by showing a converse: if the monad at hand preserves a drop equation, then it must be affine. From this, we show that the problem whether a given (drop) equation is preserved is undecidable. A converse for relevance turns out to be more subtle: preservation of certain dup equations implies a weaker notion which we call -relevance. Finally, we identify the subclass of equations such that their preservation is equivalent to relevance.

Preservation of Equations by Monoidal Monads · wovepaper