<p>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) <span class="math-container">$\bot$</span> which signifies non-termination, but then we disallow handling it, as that would allow us to implement the Halting oracle.</p>

<p>Such treatment of non-termination is a bit naive. A more satisfactory account of non-termination would use domain-theoretic semantics, or a lifting monad.</p>

CC BY-SA 4.0
2019-09-22T15:02:28.503Z
The paper [Total Functional Programming](http://www.jucs.org/jucs_10_7/total_functional_programming) that I cite in my answer argues that non termination would be best handled by codata. What do you make of that?
Henry Story
CC BY-SA 4.0
2019-09-22T16:10:44.937Z
The paper is not about non-termination per se, although it speaks about it. It's about the difference between inductive and coinductive datatypes in the context of a total programming language. These are not entirely unrelated topics, but it's not really the same thing. "Fuel" and codata are ways of *simulating* non-termination in a terminating language, but they do not address non-termination as a "native" phenomenon in a partial language.
Andrej Bauer
CC BY-SA 4.0
2019-09-23T06:20:24.907Z
Ah yes, the codata article is about creating a language that would avoiding non terminating programs, or at least those caused by folding accidentally over an infinite list.
Henry Story
CC BY-SA 4.0
2019-09-18T09:24:15.577Z
2019-09-18T09:24:15.577Z
Andrej Bauer
<p>You may be interested in <a href="https://strathprints.strath.ac.uk/60166/1/McBride_LNCS2015_Turing_completeness_totally_free.pdf" rel="nofollow noreferrer">this paper</a>. 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. He also references Eff and such.</p>

<p>It's also dependently typed, but you could do without that; most of the examples seem to not actually use the dependent typing. If you write down the simple typed version, I don't think the signature is anything fancy. It's basically:</p>

<pre><code>recursive : S -&gt; [call(s:S) : T]T
</code></pre>

<p>Where the bit in square brackets is the effect signature.</p>

CC BY-SA 4.0
2019-09-18T05:02:14.830Z
2019-09-18T05:02:14.830Z
Dan Doel
<p>In 2004 D. A. Turner argued in an easy to read article <a href="http://www.jucs.org/jucs_10_7/total_functional_programming" rel="nofollow noreferrer">Total Functional Programming</a> 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 problem algebraically, but would not make it possible to write an operating system, web server, or any process that could continue indefinitely.  That could be solved by adding codata to the language, argues the author.</p>

<p>See also a recent article <a href="https://link.springer.com/chapter/10.1007/978-3-030-17184-1_5" rel="nofollow noreferrer">Codata in Action</a> or the blog post <a href="http://blog.sigfpe.com/2007/07/data-and-codata.html" rel="nofollow noreferrer">Data and Codata</a>. </p>

<p>This indicates that non-termination is coalgebraic.
But I guess there is an interesting relation between coalgebras and effects, and indeed the paper by Andrej Bauer <a href="https://arxiv.org/pdf/1807.05923.pdf" rel="nofollow noreferrer">What is algebraic about algebraic effects and handlers?</a> has a Section 4 entitled <em>What is <strong>Coalgebraic</strong> about Algebraic Effect Handlers</em></p>

CC BY-SA 4.0
2019-09-21T21:49:15.047Z
2019-09-22T14:59:03.690Z
2019-09-22T14:59:03.690Z
Henry Story
<p>Non-termination is sometimes considered an effect.  I have been reading about algebraic effect systems (<a href="https://arxiv.org/pdf/1807.05923.pdf" rel="noreferrer">What is algebraic about algebraic effects and handlers?</a>), and I suspect non-termination (like that arising from a fixed point operator) could fit in the algebraic effect framework.</p>

<p>For instance if effects systems act like continuations, it seems easy to add a handler that supplies "fuel" for possibly non-terminating computations.</p>

<p>Another way to encode a non-termination effect might be though SKI combinators, since they are Turing complete and I think they can be presented as an algebra.</p>

<p>The programing language <a href="https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/paper-20.pdf" rel="noreferrer">Koka</a> has a non-termination effect, but it is a built in "primitive" effect.  So it's unclear to me if it could be encoded by a user in their standard effect system.</p>

<p>Can non-terminating computation be considered an algebraic effect?  If so, are there standard ways to do it?  Any references would be great.</p>

<reference-request><pl.programming-languages><functional-programming><semantics><algebraic-effects>
Can Non-termination be considered an algebraic effect?
user833970
# Can Non-termination be considered an algebraic effect?

(Asked by: username_0 on 2019-09-16)

Non-termination is sometimes considered an effect. I have been reading about algebraic effect systems ([What is algebraic about algebraic effects and handlers?](https://arxiv.org/pdf/1807.05923.pdf)), and I suspect non-termination (like that arising from a fixed point operator) could fit in the algebraic effect framework.

For instance if effects systems act like continuations, it seems easy to add a handler that supplies "fuel" for possibly non-terminating computations.

Another way to encode a non-termination effect might be though SKI combinators, since they are Turing complete and I think they can be presented as an algebra.

The programing language [Koka](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/paper-20.pdf) has a non-termination effect, but it is a built in "primitive" effect. So it's unclear to me if it could be encoded by a user in their standard effect system.

Can non-terminating computation be considered an algebraic effect? If so, are there standard ways to do it? Any references would be great.

**Tags:** reference-request, pl.programming-languages, functional-programming, semantics, algebraic-effects

---

## 3 answers

### Answer by username_1 on 2019-09-18. Score: 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 more satisfactory account of non-termination would use domain-theoretic semantics, or a lifting monad.

> **Comments:**
> **username_2**: The paper [Total Functional Programming](http://www.jucs.org/jucs_10_7/total_functional_programming) that I cite in my answer argues that non termination would be best handled by codata. What do you make of that?  
> **username_1**: The paper is not about non-termination per se, although it speaks about it. It's about the difference between inductive and coinductive datatypes in the context of a total programming language. These are not entirely unrelated topics, but it's not really the same thing. "Fuel" and codata are ways of *simulating* non-termination in a terminating language, but they do not address non-termination as a "native" phenomenon in a partial language.  
> **username_2**: Ah yes, the codata article is about creating a language that would avoiding non terminating programs, or at least those caused by folding accidentally over an infinite list.  

---

### Answer by username_3 on 2019-09-18. Score: 3

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. He also references Eff and such.
It's also dependently typed, but you could do without that; most of the examples seem to not actually use the dependent typing. If you write down the simple typed version, I don't think the signature is anything fancy. It's basically:
recursive : S -> [call(s:S) : T]T

Where the bit in square brackets is the effect signature.


---

### Answer by username_2 on 2019-09-21. Score: 2

In 2004 D. A. Turner argued in an easy to read article [Total Functional Programming](http://www.jucs.org/jucs_10_7/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 problem algebraically, but would not make it possible to write an operating system, web server, or any process that could continue indefinitely. That could be solved by adding codata to the language, argues the author.

See also a recent article [Codata in Action](https://link.springer.com/chapter/10.1007/978-3-030-17184-1_5) or the blog post [Data and Codata](http://blog.sigfpe.com/2007/07/data-and-codata.html).

This indicates that non-termination is coalgebraic.
But I guess there is an interesting relation between coalgebras and effects, and indeed the paper by Andrej Bauer [What is algebraic about algebraic effects and handlers?](https://arxiv.org/pdf/1807.05923.pdf) has a Section 4 entitled *What is **Coalgebraic** about Algebraic Effect Handlers*


---

