9
$\begingroup$

Non-termination is sometimes considered an effect. I have been reading about algebraic effect systems (What is algebraic about algebraic effects and handlers?), 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 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.

Improve this question
$\endgroup$

3 Answers 3

Reset to default
7
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • $\begingroup$ The paper 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? $\endgroup$
    – Henry Story
    Commented Sep 22, 2019 at 15:02
  • 2
    $\begingroup$ 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. $\endgroup$
    – Andrej Bauer
    Commented Sep 22, 2019 at 16:10
  • $\begingroup$ 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. $\endgroup$
    – Henry Story
    Commented Sep 23, 2019 at 6:20
3
$\begingroup$

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.

Improve this answer
$\endgroup$
2
$\begingroup$

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 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 or the blog post Data and Codata.

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? has a Section 4 entitled What is Coalgebraic about Algebraic Effect Handlers

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.