Do we want total functions

Issue, or potential issue

We have pure functions, but we don't have a way of defining a total function, which is guaranteed to halt. The question is, do we want total functions, or is their use-case too specific?

Potential solutions

Add total keyword. A total function is defined on all inputs and therefore halts on all inputs. Therefore, a total function:

Never returns an error.
We can guarantee that it halts on all inputs by for instance:
- checking that is is defined on every (discrete) possible input, for instance, an enum.
- or somehow using induction to prove it always halts.

A function that is not total, is a "partial function".

consider the following examples:

def neg(x: Bool): Bool => not x

This returns the negation of its input, is both pure and total.

def f(x: Int): Int =>
    call_count <- call_count + 1 
    return 100 / x

Is neither pure nor total. It is not defined for the input 0, and it performs a side effect. Though in the current implementation of Mamba, this is still seen as pure, as it adhere to the rules of the language for being pure (see #110 ).

def f(x: Int): Int => 
    call_count <- call_count + 1
    return x

Is total but not pure. It is defined on all inputs.

Code-wise I think having a total token would not hinder the readability of the language too much. I.e. def pure total f (x: MyClass) => ... is still readable.

JSAbrahams / mamba

Do we want total functions #111

Issue, or potential issue

Potential solutions