(Daan here, creator of [Koka](https://github.com/koka-lang/koka)

This is an interesting point and comes down to the question -- what is an effect really? I argue that effect types tell you the type signature of the mathematical function that models your program (the denotational semantics). For example, the function

  fun sqr(x : int) : total int { x*x }

has no effect at all. The math function that gives semantics to `sqr` would have a type signature that can be directly derived from the effect type:

  [[int -> total int]]  = Z -> Z

(with Z the set of integers). Now, for a function that raises an exception, it would be:

  [[int -> exn int]] = Z -> (Z + 1)

That is, either an integer (Z), or (+), a unit value (1) if an exception is raised. Similarly, a function that modifies a global heap h, would look like:

  [[int -> st<h> int]] =  (H,Z) -> (H,Z)

that is, it takes an initial heap H (besides the integer) and returns an updated heap with the result.

Now, non-termination as an effect makes sense: a function like "turing-machine" may diverge, so:

  [[int -> div int]] = Z -> Z_\bot

That is, its mathematical result is the set of integers (Z) together with an injected bottom value that represents non-termination. (note: We don't use "Z + \bot" here since we cannot distinguish if a function is not terminating or not (in contrast to exceptions)).

In a language like Haskell every value may not terminate or cause an exception -- that is a value `x :: Int` really has type `Int_\bot`, and we cannot replace for example `x*0` with `0` in Haskell.

Note that in almost all other languages, the semantic function is very complex with a global heap etc, any function `[[int -> int]]` becomes something like `(H,Z_32) -> (H,(Z_32 + 1))_\bot`. This is the essence of why it much harder for compilers and humans to reason about such functions (and why effect types can really help both programmers and compilers to do effective local reasoning)

I'm wondering if you've found it useful in practice to distinguish between total and possibly-diverging functions?

It seems like it's the sort of thing that's useful in something like Agda, where you use the existence of a function (without running it) to prove that its result exists. (The type is inhabited.) Or so I've read; I haven't used it.

But if you're going to run the program, you typically want to know if a function will return promptly, and a total function could still spin for a million years calculating something, in a way that's indistinguishable in practice from diverging.

In practice, I have not (yet) found many great use cases for the distinction in Koka. It is nice to have "total" functions, but "pure" (exceptions+divergence) is still a good thing (and what Haskell gives you). And like you say, in practice we can easily have functions that just take a long long time to compute.

Still, it is a good extra check and I can see more use for the `div` effect for future verification tools where total functions can be used as a predicates (but non-terminating ones cannot).

Good to know. At compile or verification time, it seems like you could get the same problem again, though? We want our compiles to finish promptly, and a slow, total predicate could hang.

Which is to say, a possibly-diverging function seems okay to use even by a verification tool, so long as it finishes quickly in practice. Having some notion of analysis-time-safe predicates seems useful but it doesn't seem to map cleanly to being able to prove termination?

I have found total checks in languages like idris helpful, but really only for catching small mistakes that I've made (for example, recursing on the original argument)

If your language has equality proofs, for example `a = Int` then, if your language is non-total I can prove anything by divergence. So I can prove `Int = String`. This is still type-safe as long as you don't erase the proof, because you can never use the invalid proof because your program will diverge.

So if you want to be type-safe but you still want to be able to erase proofs, your proofs have to be total.

I never understood this one. I mean obviously a kind compiler should warn you against using

    while true { }

and

    while i < 5 { i—-; }

but in general, I don’t find distinction between “this infinite loop terminates” (e.g. an event loop) and “this code obviously terminates but not in the lifetime of this universe” (e.g. computing Ackermann(5)) to be that useful.

It's primarily useful for theorem proving, where a nonterminating argument corresponds to circular or otherwise unfounded reasoning.

It's also useful because, in practice, we don't accidentally write code that "obviously terminates but not in the lifetime of this universe" as often as we accidentally write nonterminating code, so a lot of mistakes can still be caught by termination checking.

...that cannot be determined by the system (and must be specified by the user).

Just to add to this: Koka can (obviously :-)) not always determine if a function will terminate or not so it generally adds a `div` effect whenever there is the possibility of infinite recursion.

However, since most data types in Koka are inductive, any recursion over such inductive data types are still inferred to be always terminating.

In practice, it looks like about 70% of a typical program can usually be `total`, with 20% being `pure` (which is exceptions + divergence as in Haskell), and the final 10% being arbitrary side effects in the `io` effect.

these numbers are very useful to me even as a Python programmer, as they (somewhat) line up with my intuitions about how much of our programs can be expected to be written as (Python-) pure transforms, vs imperative shells. It's cool to think about a language being able to tell me this directly.