[daanx]

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.

[ledauphin]

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.