Inductive Reasoning About Effectful Data Types

TY - GEN

T1 - Inductive Reasoning About Effectful Data Types

AU - Filinski, Andrzej

AU - Støvring, Kristian

N1 - Conference code: 12

PY - 2007

Y1 - 2007

N2 - 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 failure-continuation 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.

AB - 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 failure-continuation 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.

U2 - 10.1145/1291151.1291168

DO - 10.1145/1291151.1291168

M3 - Article in proceedings

SN - 978-1-59593-815-2

T3 - SIGPLAN Notices

SP - 97

EP - 110

BT - ICFP 07

PB - Association for Computing Machinery

T2 - ACM/SIGPLAN International Conference on Functional Programming

Y2 - 1 October 2007 through 3 October 2007

ER -