Inductive reasoning about effectful data types

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 than partiality. We further show how these principles can be integrated into logical-relations arguments, and obtain as a particular instance a general and principled proof that the success-stream and failurecontinuation models of backtracking are equivalent. As another application, we present a monadic model of general search trees, not necessarily traversed depth-first. The results are applicable to both lazy and eager languages, and we emphasize this by presenting most examples in both Haskell and SML.

• Type: Conference
• Year: 2007
• Where: ICFP
• Authors: Andrzej Filinski, Kristian Støvring
• Keywords: General Search Trees, ICFP 2007, Monadic Effects, Monadic Model, Programming Languages