7

Non-termination can be considered an algebraic effect up to a point. It's an exception that cannot be handled. More precisely, we may introduce a nullary operation (constant) $\bot$ which signifies non-termination, but then we disallow handling it, as that would allow us to implement the Halting oracle. Such treatment of non-termination is a bit naive. A ...


2

You may be interested in this paper. It describes things in terms of monads, but the idea is that you define an 'effect' of making a recursive call. Then appropriately typed functions can be interpreted as recursive definitions. Note for instance on page two where he refers to the, "generic effect," which is something you'll see in work on algebraic effects. ...


1

In 2004 D. A. Turner argued in an easy to read article Total Functional Programming that non termination is a problem with interpreting languages like Haskell purely mathematically, but that to resolve it one needed to add codata types. A pure functional language where no function was non-terminating (resolved to ⊥) would enable clear reasononing about the ...


Only top voted, non community-wiki answers of a minimum length are eligible