Recursive functions

[RunDevelopment]

Right now, recursive function are not supported. This is because recursive function are tricky to implement in a type system. One of the main problems is that they are very hard to type check. Let's look at an example:

def fact(n: int(0..)) = match n { 0 => 1, _ as x => fact(x - 1) * x };

This is a very simple example of a factorial function for unsigned integers. The problem is that x is the type int(1..), so x-1 is int(0..) which is the same as the input type. So to determine the output type of fact(int(0..)), we need to know the output type of fact(int(0..)).

One way to solve this would to examine the call stack and detect cycles. Suppose we want to evaluate fact(int(2..)). How would the call stack look like?

fact(int(2..))
fact(int(1..))
fact(int(0..))
fact(int(0..))
...

So we see a cycle of length 1 for fact(int(0..)). One way to resolve the cycle is to iteratively refine the output type until it converges.

• We define never as the starting output type of fact(int(0..)). We now replace all recursive calls to fact(int(0..)) with never, so we get the expression match n { 0 => 1, _ as x => never * x }.
• This evaluates to 1 which will be our next output type. The process repeats with match n { 0 => 1, _ as x => 1 * x }.
• This evaluates to int(1..) which will be our next output type. The process repeats with match n { 0 => 1, _ as x => int(0..) * x }.
• This evaluates to int(1..). This is the same type as in the previous iteration, so the output type of fact(int(0..)) has successfully converged to int(1..).

Since we now know the output type of fact(int(0..)), it is trivial to determine the output types of fact(int(1..)) and fact(int(2..)).

However, even determining the output type of a recursive function as simple as this, isn't easy to implement. Factorial is also a simple example considering that it (1) has a cycle of length 1 and (2) also recurses into itself once per invocation.

Let's look at a recursive implementation of the Fibonacci function for a more complex example:

def fib(n: int(0..)) = match n { 0 | 1 => 1, _ as x => fib(x - 1) + fib(x - 2) };

Since this function has exponential time complexity with memoization, let's assume that we implemented efficient memoization (or maybe it should be called call de-duplication?). Let's see the de-duped call stack for fib(int(4..)):

fib(int(4..))
fib(int(3..)) fib(int(2..))
              fib(int(1..)) fib(int(0..))
                            fib(int(0..))
                            fib(int(0..))
                            ...

The length-one cycle of fib(int(0..)) can be resolved just like with fact(int(0..)), so let's try that:

• We start with never again, so we get match n { 0 | 1 => 1, _ as x => never + never }.
• This evaluates to 1. The pattern is pretty obvious again, so let's just list out the next couple of iteration output types:
• Next is int(1..2) (so 1 or 2).
• Next is int(1..4).
• Next is int(1..8).
• Next is int(1..16).
• Next is int(1..32).

We can see a pattern here, but this is bad news. While the output type will clearly converge to int(1..inf) eventually, it will only do so after (mathematically speaking) infinitely many iterations. This is a problem.