In this paper, I show that general recursive definitions can be represented in the free monad which supports the ‘effect’ of making a recursive call, without saying how these calls should be executed. Diverse semantics can be given within a total framework by suitable monad morphisms. The Bove-Capretta construction of the domain of a general recursive function can be presented datatype-generically as an instance of this technique. The paper is literate Agda, but its key ideas are more broadly transferable.
|Name||Lecture Notes in Computer Science|
|Conference||12th International Conference on Mathematics of Program Construction (MPC 2015) |
|Period||29/06/15 → 1/07/15|
- monad morphisms
- total functional programming
- general recursion