One Monad to Prove Them All (Functional Pearl) https://arxiv.org/abs/1805.08059
#Coq で #Haskell プログラムの性質を証明するケーススタディとして無茶苦茶面白い。 partiality などの effect を扱うためにデータ型の各成分をモナドの値にしたいが、 モナドをパラメータ化すると strictly positive の検査に失敗するようになってしまうので、 コンテナの構造でパラメータ化して、 コンテナで定義される関手の自由モナドとして扱う話がメインで、他にもネストした帰納的型になるのでCoqがデフォルトで生成する induction principle が使えず、独自の induction princle を定義したりとか、ハマりどころとその解決が物語仕立てで解説されている。
具体例としてリスト二つで表現するキューの性質の証明や、応用としてCurryの非決定性や確率的プログラミングの話も少し。
物語仕立てで書かれているので気楽に読め、また参考文献がすべて Book として参照されていたり、コードの図表が Scroll になってるのも雰囲気が出てる。 こういう趣向は A Play on Regular Expressions https://sebfisch.github.io/haskell-regexp/regexp-play.pdf を思い出すね（どっちも Functional Pearl ）。