Introduction to Functional Programming

Objects and Compatibility

Learning Objectives

You understand primitive types in .
You understand the idea of type equivalence (), and can justify an equivalence mathematically.
You can recognize common equivalences (e.g. swapping pairs, currying/uncurrying, re-ordering arguments).
You understand why equivalent types are not literally “equal” types in a programming language.
You can encode simple custom data types using sums and products, and define their data constructors.
You can distinguish general recursion from structural recursion via a recursor.
You know of the recursor for natural numbers, and can use it to implement primitive recursive functions.

Primitive Types

In , primitive types include the booleans, integers, characters, unit type, functions, products, sums and lists. With these types, we can build more complex types by composing them, e.g.

is the type of (possibly partial¹) functions that map integers to integers.
is the type which contains lists of integer lists.
is the type of products, i.e. pairs, whose elements are an integer and an integer list.
is the type of coproducts, i.e. sums, whose elements are either an integer or a boolean.

Each of these types is fundamentally different in the sense that there isn’t a bijection between any distinct pair. However, this rule is not universal, there do exist types which correspond bijectively, for example all of the following:

For example, has four elements, but so does . has four representatives which all behave differently, i.e. have a different function graph, compared to one another. After defining the notion of equivalence, you get to construct some equivalences including the one between pairs of booleans and functions between booleans.

Equivalence

A bijection between types is called an equivalence and denoted with the symbol . An equivalence always comes with two functions, one for the forward direction and one for the reverse direction. In addition, an equivalence has two laws: the forward direction is the inverse function of the reverse direction and vice versa.

Examples

Let’s actually construct some equivalences between types in . As a first example, let’s show that elements in a pair can be swapped.

No files opened Select a file to edit

The proposed functions and do appear to act correctly based on the result of computing g (f (true, 10)), but we can do better — let’s prove the equivalence laws!

Here’s another example which demonstrates that the order of arguments doesn’t matter, or stated using integers and booleans,

Writing the definition for f : (Int -> Bool -> Int) -> Bool -> Int -> Int and g : (Bool -> Int -> Int) -> Int -> Bool -> Int is straight-forward:

No files opened Select a file to edit

Proving that the above and form an equivalence is left as an exercise for the reader.

We will next look at a classic example of equivalence between different styles of calling functions.

In mathematics, one typically writes for applying a function to two arguments. The two arguments are often “grouped together” as a pair , so the function would have type However, as you have learned by now, in functional programming one typically writes arguments by chaining arrows: — so it shouldn’t come as a surprise that these styles are equivalent.

From now on, we use the notation in mathematical text to mean or f h b n in the functional programming sense. It should be clear from the context whether a function takes a pair/tuple argument or takes its arguments in a Curried way. As the variants are equivalent, making a destinction between the two explicitly should be unnecessary when reading mathematical text combined with code.

More equivalences

Think about why the following equivalences between infinite types are valid:

However the following is not an equivalence:

Start by thinking about why is an infinite sequence of zeros and ones. Next, you may want to explore Cantor’s diagonal argument on Wikipedia for a set-theoretic proof of the analogous claim.

Loading Exercise...

Custom Data Types

, unlike most functional programming languages, doesn’t support creating new data types, like enumerations or structures. Instead, one uses type declarations or aliases. However, many interesting data types are recursive, but type declarations in don’t support recursion, so this approach won’t work for defining recursive types.

Let’s start with a basic example: traffic lights.

No files opened Select a file to edit

We define the type alias TrafficLight = Unit + Unit + Unit (parenthesized as (Unit + Unit) + Unit) and three constructors: red, yellow, green which return traffic lights. The repr function shows how one matches nested sums in — notice that there is no fancy syntax sugar for it.

A constructor is therefore nothing special: any function that returns a TrafficLight is a constructor for it. red, yellow and green are just convenient ways to construct any and all elements of TrafficLight.

Loading Exercise...

Enumerations With Data

Enumerations in functional languages can also carry data. The data is naturally provided when calling the constructors. Matching with case then let’s us use that data.

No files opened Select a file to edit

Nothing stops us from storing functions inside custom types, let’s do that as well.

No files opened Select a file to edit

As a reminder: sum types with more than two summands, like A + B + C are parenthesized as (A + B) + C, i.e. + associates left.

Loading Exercise...

Algebra of Types

Product types, i.e. pairs, are intuitively understood from the perspective of cartesian products of sets. The type has four elements corresponding with the elements of .

Like product types, sum types are a convenient method of constructing types, but why are they called “sum” types. If we took sum types as simply unions of sets, we would end up in trouble, as would be treated as the set and have just two elements instead of the four inhabitants of : inl false, inl true, inr false and inr true.

Instead of a regular union, we take the disjoint union (), i.e. we first “color” both sets with distinct colors and then take their union.

The coloring can be defined by giving a unique number to each color and pairing up that color and the value.

Taking a disjoint union of two sets as the counterpart to taking a sum of two types is the natural choice.

Next, to define the algebra of types, we need so called neutral elements of products and sums. These are called and and correspond to the types Unit and Empty respectively.

The type Empty is defined in the standard library as the polymorphic function forall X, X. We will cover polymorphic types in the next chapter.

We would like to take to be the “type of all types” and to be the product of types, however we end up in trouble. First, the notion of a “type of all types” is problematic, as its interpretation would have to be a set leading to impredicativity issues. Secondly, the notion that the types in are equal is also problematic as we have learned already. To rectify these issues, we replace “set” by “type” and by equivalence when talking about neutral elements in the algebra of types.

Next, we show associativity of product types, where i.e. . We start with concrete types for now to make things easier: . As usual, we construct functions going both ways.

No files opened Select a file to edit

Exercise for the reader: f and g satisfy the equivalence laws.

As Unit is claimed to be the neutral element of products, we construct the equivalences using the following functions

Next, your task is to prove the distributivity laws that tie product and sum types together.

There is a lot more interesting mathematics regarding the algebra of types that is not covered here. For example function types have the property of exponentiation: can be viewed as and it’s not hard to prove that . To learn more about exponential types, check chapter 9.5 in Category Theory for Programmers.

Loading Exercise...

Natural Numbers

Natural numbers are perhaps the most simple yet interesting object in mathematics. They form a set of infinite cardinality (size) and are characterized by just three simple functions:

The constant (function) zero.
The successor function, which adds 1.
The recursor, which let’s us match a natural number with two branches.

doesn’t have natural numbers as a primitive, but we can encode them in a silly but straight-forward way: using lists.

In short, we use a list of units to represent a natural number. It’s horribly inefficient but it works for small numbers (< 1000). For example, the number zero is an empty list, one is the list [()], two is [(), ()] and so on.

No files opened Select a file to edit

To encode an integer as a Nat, i.e. a list of units, we map all negative integers to zero and positive integers to corresponding natural numbers.

No files opened Select a file to edit

Loading Exercise...

Recursors

Recursors are functions that work like match-expressions. However, what makes recursors more general is that they let the branches use “recursive results”. For example, fold is the recursor of — you guessed it: lists! It takes in two “branches”: the empty list case, and the non-empty recursive case. The accumulator in the cons branch is the recursive result of the recursor.

Similarly, the recursor for natural numbers takes in two functions: the zero function, and the recursive step function. We can define the recursor in for the silly natural number type as follows:

No files opened Select a file to edit

Don’t worry about the “forall” for now, it’s explained in the next chapter on polymorphism.

As we can see, natural numbers can be implemented as lists, and the recursor by recursively “folding” over the list. The key property of the recursor is that unlike general recursion that we learned in the previous chapters, the recursor always terminates. The variable name ih (induction hypothesis) in the code refers to the recursive result for the predecessor. The recursor is in fact a kind of induction principle.

Some programming languages (such as Agda, Idris 2, Lean and Rocq), where functions in the core calculus must be total, attempt to convert general recursive definitions to a more general version of the recursor, which implements structural recursion. In these languages the recursor can be derived for every algebraic data type that is accepted²!

Functions that can be implemented using only the recursor (and constructors, such as zero and succ) are called primitive recursive, and this class of (total) functions is large but limited compared to general recursion. One well-known example of a non-primitive recursive³ total function is the Ackermann-Péter function written as follows:

import nat

iszero : Nat -> Bool
iszero = fun n : Nat, rec Bool n true (fun xs : Nat, fun ih : Bool, false)

pred : Nat -> Nat
pred = fun n : Nat, rec Nat n zero (fun xs : Nat, fun ih : Nat, xs)

ack : Nat -> Nat -> Nat
ack = fun a : Nat, fun b : Nat,
    if iszero a then
        succ b
    else if iszero b then
        ack (pred a) one
    else
        ack (pred a) (ack a (pred b))

Loading Exercise...

Footnotes

supports general recursion, so it is easy to accidentally define a function that never returns — which makes it partial. This means that the type arrow in is not the same as what we have in mathematics. However, we aim to write total functions to avoid unwanted infinite loops, or to make it easier to handle errors. ↩
One of the requirements for a valid data type is called “strict positivity”. Strict positivity ensures that the recursor is a total function. Here’s an example of a non strictly-positive data type in Haskell. It has a non-positive constructor Bad which takes in Bad -> Bad where, because the data type being defined occurs in a “negative position”
```
data Bad = Bad (Bad -> Bad)

instance Show Bad where
  show (Bad _) = "BAD"

getFun :: Bad -> (Bad -> Bad)
getFun (Bad f) = f

omega :: Bad -> Bad
omega f = (getFun f) f

loop :: Bad
loop = omega (Bad omega)

-- We have an infinite unfolding
-- loop = omega (Bad omega) = (getFun (Bad omega)) (Bad omega) = omega (Bad omega) = loop
```
You can read more in the Agda Wiki or in Rocq Docs. ↩
Source ↩

← Simplification and Normalization

Polymorphism →