Recursion and recursive thinking

Recursion

As you have learned in the previous chapters, a key difference between functional and imperative programming languages is immutability. This usually forces us to rethink e.g. iterative problems in a more mathematical fashion — quickly leading to recursion.

For example, consider calculating the sum of integers from to . In an imperative programming language, a typical solution could look like this:

int sum = 0;
for (int i = 1; i <= n; ++i) {
    sum += i;
}

However, if we attempt to translate this directly to , or any functional language for that matter, we quickly run into issues. First of all, there is no for or while expression in , and even if there were, we still wouldn’t have a way to update the values of i and sum as we can’t mutate variables in . It’s worth noting that many functional programming languages support something¹ that closely resembles the above C-code, it just requires a bit of getting used to.

An idiomatic implementation in could look something like this:

sumTo : Int -> Int
sumTo = fun n : Int,
    if n <= 0 then 0 // (1)
    else n + sumTo (n - 1) // (2)

In this code, instead of using a loop, we call the function being defined within its definition, which is called recursion. Substituting loops with recursion is very common when translating imperative code to functional code.

Recursive (or inductive) thinking is characterized as follows:

• We begin by defining a function that takes an input x.
• By assuming that the function being defined works correctly for strictly smaller inputs than x, we are allowed to make recursive calls with smaller inputs to compute the desired output for the current input x.

For example, on line (2), we use the sumTo function recursively with the assumption that it returns the correct result for inputs strictly smaller than the current input, i.e. n — this assumption is often called an inductive hypothesis. From this, we know that the “correct thing to do” is to add our n to the previous result — because the previous result is correct by the induction hypothesis.

The reason recursion works, is mathematical induction (or specifically induction over natural numbers in this case):

1. We show the base case (1) is correct, i.e. sumTo 0 evaluates to 0.
2. Inductive/recursive case (2): assuming sumTo (n - 1) is valid because n - 1 is strictly less than n, we produce the result of n + sumTo (n - 1).

Strictly speaking induction also requires that the concept of “smaller” (a less-than relation) is well-founded. Conveniently, most data types we run into in programming have a well-founded less-than relation. As a nonexample, rational numbers with the usual less-than relation is not well-founded, so inductively defining a function for a rational number can not recursively evaluate itself at .

The Linked List data type

In addition to primitive data types, implements the list data type. It is implemented as a linked list, meaning that each element refers to the next one. A list consists of 0 or more elements of the same type but in this chapter we’ll be using the list of Ints denoted by List Int or [Int]. Lists of type T have two constructors: cons : T -> [T] -> [T] and nil T : [T]. Notice how the cons constructor takes another list of the same type as the second argument — this makes list a recursive data type.

doesn’t have a Hindley-Milner type system nor unification of any kind. It requires type parameters explicitly when it comes to constructors like nil. An alternative way to write an empty list of type T is [:T].

The notation ..= is syntax sugar for an inclusive range of integers. Likewise, .. is used for an exclusive range.

To deconstruct or pattern match a list in , we use the lcase expression. The lcase has two branches (starting with the | character), the nil branch, matching an empty list, and the cons head tail branch, matching a non-empty list. In the spirit of the language, both of the branches must be present and therefore a list must always be matched exhaustively.

If you don’t want to bind a value to a variable in , you can use an _ where the variable name would go

Lists and Recursion

Since the list is a recursive data type, it makes sense that a lot of list operations are implemented with recursion.

A sum over a list of integers can be implemented as shown above. The nil branch corresponds to the base case (sum of an empty list is zero) and the cons branch corresponds to the recursive case, where the sum of a list is defined as the value of the first element plus the sum of its tail.

h and t stand for head and tail. Other common variable names used after cons are x and xs.

Unlike with arrays, which you can easily index with an arbitrary offset, lists must always be accessed from the beginning, one element at a time. This means that accessing an element at an arbitrary index and many other list operations are generally . In functional programming, if you find yourself in a situation where you’re trying to index a list, it’s perhaps a good idea to think about your approach for a second.

pub fn sum_loop(mut to: i32) -> i32 {
    let mut ans = to;
    to -= 1;
    while to != 0 {
        ans += to;
        to -= 1;
    }
    ans
}

int sum(int to) {
    int sum = 0;
    while (to) {
        sum += to;
        to--;
    }
    return sum;
}

Higher-order functions and mapping over recursive structures

Since lists are a recursive data structure, and we often want to call a function on its elements exactly once, higher-order functions emerge naturally.

As we know, functions are not restricted to taking regular values⁴ as arguments. They can also take functions as arguments. Higher-order functions allow programmers to, for example, “customize the behavior” of a function.

One of the more common functions in functional style code is the map function, which applies a function to each element in a collection returning the “mapped” version of the collection. Below is an example of the map function for our List of Ints.

map : (Int -> Int) -> [Int] -> [Int]
map = fun f : (Int -> Int), fun xs : [Int],
    lcase xs of
    | nil => xs
    | cons h t => f h :: map f t

This map function takes in a function with type signature , but it could theoretically also take in or (or really a function of any return type).

While map “preserves” the structure (i.e. the order and shape) of the collection, there exist also a plethora of useful functions that “alter” the structure, for instance, the filter function that takes in a predicate and returns a collection that consists only of elements in the original collection for which the predicate returns true.

Error Handling

Error handling, at compile time and runtime, is something functional programming languages tend to be really good at. When it comes to errors that are raised during runtime, most languages have a try-catch mechanism to handle them. This is not the case with functional languages, because functions can’t “return early” to raise an error — control flow is more visible in functional languages.

As always, there is a way to raise and catch errors, but the style is quite different compared to Python, Java, JavaScript etc. Errors are implemented as ordinary data, typically using sum types called Option or Result, which are covered in a later chapter. Such a style is also present in languages such as Rust and Java, where instead of raising an error, the function returns Option::None or Result::Err.

One of the reasons that sum types are not used everywhere is that they add more complexity and work for the caller to handle the different cases. Even in functional languages some functions prefer not to handle errors and panic (i.e. crash) instead. Such functions belong to the class of non-total functions.

Exceptions and Panicking

supports exception with using panic terms. The term panic T msg tells the type checker that this term has type T — which can be any type you choose.

When evaluating a panic term, all computations are halted and the evaluator immediately returns. To the outside, this looks like the panic term “infects” all other computations causing the panic term to “bubble up”. Because the panic halts the program, no computation can deduce anything from its value, so it’s not even considered as a value.

doesn’t have a way to handle exceptions, and that’s why they are called panics.

To demonstrate the idea, let’s look at the head function for lists.

head : [Int] -> Int
head = fun xs : [Int],
    lcase xs of
    | nil => panic Int "head called on empty list"
    | cons h _ => h

head is implemented in a fashion that panics on empty lists.

In the following code, where head is used, the panic term infects the computation + 10 which means that evaluating main returns the panic term.

main : Int
main = head [:Int] + 10

The code type checks because head [:Int] : Int and so adding another integer results in an integer. The type checker is not aware of the panic and cannot deduce whether it occurs or not.

total_42 : Int -> Int
total_42 = fun _ : Int,
    lcase [42:Int] of
    | nil => panic Int "unreachable"
    | cons answer _ => answer

Totality

As mentioned in the overview, total functions are those relations which map every input to at least one output.

Reminder: all functions in mathematics are both functional and total.

Functions like head and tail from the standard library are non-total because they panic on empty lists, i.e. they do not map [] to any output. This is a widely accepted as a “feature and not a bug” even though it’s completely incorrect and absurd from a mathematical perspective. Total versions of head and tail could be created by returning a default value for empty lists (or a junk value as is preferred in proof assistants⁵) or using the aforementioned sum types Option or Result.

Another cause of non-totality in programming is the use of recursion without a base case. Defining such a function is comparable to writing an equation of the form — calculating the value of any diverges computationally. Even if there “seemingly” is a base case, totality requires termination on all inputs.

factorial : Int -> Int
factorial = fun n : Int,
    if n == 1 then n
        else n * factorial (n - 1)

Consider the implementation of factorial in the above code, it does not return a value for inputs n <= 0. For those inputs, the function ends up in an infinite chain of recursive calls.

By this counterexample, we’ve shown that our poorly written implementation of factorial is non-total.

Showing that a function is non-total is actually rather difficult or even impossible in general, as famously proven by Alan Turing in 1930s. This is why a programming language or a type system cannot decide whether a function is total in general.

There are still many cases where totality is guaranteed, for example when doing structural recursion. Even more complex recursive functions can still be proven to be total. Turing’s proof simply showed us that no single algorithm can decide correctly whether a program halts or a function is total across all inputs.

pub fn sum_loop(mut to: i32) -> i32 {
    let mut ans = to;
    to -= 1;
    while to != 0 {
        ans += to;
        to -= 1;
    }
    ans
}

pub fn add1(x: i32) -> i32 {
    x + 1
}

Footnotes