In functional programming, monadic characterizations of computational effects are normally understood denotationally: they describe how an effectful program can be systematically ...
We present a pair of reasoning principles, definition and proof by rigid induction, which can be seen as proper generalizations of lazy-datatype induction to monadic effects other...