2.
Function Fundamentals
Written by Massimo Carli
In Chapter 1, “Why Functional Programming”, you learned that functional programming means programming with functions in the same way that object-oriented programming means programming with objects.
Objects and functions are very different beasts. Objects, at first sight, probably look closer to what you see and interact with every day. Think of your car, for instance. It has some properties like brand, color, engine and size. You use property values to distinguish a Ferrari from a Fiat 500. When you write your code, you model objects using classes. For instance, you define a Car
class like this:
class Car(
val brand: String,
val color: Color,
val engine: Engine,
val size: Int,
var speed: Int
) {
fun drive() {
// Driving code
}
fun accelerate() {
speed += 1
}
}
The state of an object is the set of its properties’ values. Objects also interact, sending messages to each other. This interaction happens by invoking something called methods.
You can interact with a Car
instance by invoking the accelerate
method to increase its speed, which then changes its state.
Classes allow you to define what the methods are. The concept of a class is just the first tool you have to describe your application in terms of objects. Many other concepts and tools help define what object-oriented programming is, such as interface, inheritance, polymorphism and aggregation.
But what about functions? Are functions also close to what you see and interact with every day? What does it really mean to program with functions? Is there something similar to the concept of a class with functional programming?
Unfortunately, you can’t answer all these questions in a single chapter. To understand it, you need to really understand what a function is, which requires the knowledge of some fundamental concepts of category theory. This chapter will give you that knowledge! What you’ll learn in this chapter will give you a strong foundation for the rest of the book.
In this chapter, you’ll learn:
- What category theory is.
- How a category is related to the concept of a function.
- The useful concepts of initial and terminal objects, using logic as a fun example of a category.
- What the relationship is between category theory and functional programming.
- What the concept of type has to do with sets.
- Where the Kotlin
Nothing
andUnit
types come from. - What it means for an object to be an element of a set in the context of category theory, and therefore, functional programming.
These are all very theoretical concepts, but you’ll see some practical examples using the Kotlin language.
Note: If you’re not confident with Kotlin, our Kotlin Apprentice book is the best place to start.
Note: The concepts in this chapter might look theoretical and, sometimes, not very intuitive. Don’t worry! It’s perfectly normal, and even expected, to read this chapter multiple times to digest the content that will help you to better understand many other concepts of functional programming in this book.
What is a function?
You might already have an initial idea about what a function is from the math you learned in school. You may remember that a function is a way to describe how to calculate an output given an input value, like in Figure 2.1:
For instance, the function:
fun twice(x: Int) = 2 * x
Returns an output value that’s double the value you pass in as an input. That’s a representation of a mathematical function.
In the context of functional programming, a function is something more abstract that’s not necessarily related to computation. A function is a way to map some values to others. The bunch of all the values a function accepts as input is the domain of the function. The bunch of all the values the function returns as output is the range of the function. Domain and range can also be the same bunch of values.
Note: It’s important at this point to emphasize the term bunch of values. This is because the term set, as you’ll see soon, is something that gives some kind of rules to that bunch. For instance, a set can include an object or not, and it can’t include the same object more than once.
Figure 2.2 better represents what a function is:
- For each value in the domain, there’s one and only one value in the range. This implies that the function always returns a value for inputs in its domain.
- The function
f
can map multiple values in the domain to the same value in the range. - By definition, the function has meaning for each value in the domain, as you’ll see later. This might seem obvious, but it’s a crucial concept to understand.
Exercise 2.1: Can you write an example of a function mapping distinct values in the domain to non-distinct values in the range, like
f(b)
andf(c)
in Figure 2.2?Give it a try, and afterward, check the challenge project for a solution to see how you did. You can find hints and an explanation of the solution in Appendix B, “Chapter 2 Exercise & Challenge Solutions”.
Functions like twice
mapping distinct values in the domain to distinct values in the range have some interesting properties. As you’ll see later, the most significant is that they have an inverse function. An inverse function maps the values in the range back to the domain.
Exercise 2.2: Can you write the inverse function of
twice
? What are the domain and range for the inverse function? Check out the challenge project and Appendix B for the solution.
Another simple and useful exercise is to define the domain and range for twice
in the previous example:
fun twice(x: Int) = 2 * x
In that case, you have what’s shown in Figure 2.3:
In this exercise, you’ve done something that’s not as obvious as it appears because you used the set of all the Int
values as the domain and range for the function f
. But what is Int
? What’s the relation of the Int
type with the bunch of things mentioned earlier?
To really understand all this, it’s time to introduce category theory.
Note: If you’ve heard category theory is intimidating, don’t be scared. This book is here to help. :] Soon, you’ll realize how understanding what a category is will help you assimilate many critical concepts about functional programming. Again, feel free to read this chapter multiple times to make this process easier. This book will go over only what you really need, and it’ll be a lot of unexpected fun.
Introduction to category theory
Category theory is one of the most abstract branches of mathematics, and it’s essential here because programming is one of its main applications. It’s also important to start with the definition of category.
A category is a bunch of objects with connections between them called morphisms. Categories follow three rules:
- Composition
- Associativity
- Identity
You can picture an object like a dot with no properties and no further way to be decomposed. A morphism is an arrow between two objects like in Figure 2.4:
In this image, you:
- Have objects named
a
,b
andc
. - Define two morphisms between
a
andb
and one morphism betweenb
andc
. - Assign the names
f1
andf2
to the morphisms betweena
andb
and the nameg
to the morphism betweenb
andc
.
Objects and morphisms are the primitive tools you can use to describe every possible concept about category theory.
As mentioned earlier, objects and morphisms need to follow some rules that will lead you to other fundamental functional programming concepts. It’s time to study them in detail.
Composition
A bunch of objects and arrows don’t make a category; they also need to follow some important rules, and composition is probably the most significant.
Look at Figure 2.5:
In this image, you have:
- The objects
a
,b
andc
. - The morphism
f
froma
tob
. - The morphism
g
fromb
toc
.
The composition rule says that for every object a
, b
and c
and every morphism f
and g
, as shown in Figure 2.5, the category must have a morphism from a
to c
. You represent this as g◦f
between a
and c
, which is the composition of f
and g
. You read g◦f
as “g after f”, where the small circle ◦
represents the composition.
For a Kotlin example, if f
is your twice
and g
is triple
, then g◦f
might look like:
val `g◦f`: (Int) -> Int = { triple(twice(it)) }
Note: An analogy with LEGO® makes the definition of the composition property for a category easier to understand. Imagine an object of a category is a LEGO® brick. Being able to attach a LEGO® brick to another is equivalent to having a morphism between them. In this case, composition means you can attach one LEGO® to another to get another LEGO® component that is the composition of the two bricks.
Associativity
The associativity rule is similar to the one you studied back in school about addition or multiplication. Look at the following image:
Here, you have:
- The objects
a
,b
,c
andd
. - The morphism
f
froma
tob
. - The morphism
g
fromb
toc
. - The morphism
h
fromc
tod
.
The associativity rule says that for every object a
, b
, c
and d
and morphism f
, g
and h
(like in Figure 2.6), the following equivalence must be true:
This means that if you do the composition of f
, g
and h
, it doesn’t matter if you first compose f
to g
or g
to h
. Looking at Figure 2.6, this also means that, with those objects and morphisms, there must be a morphism from a
to d
, which you can obtain by either composing f
with h◦g
or composing g◦f
with h
.
Continuing with the previous example and quadrupling h
, this means:
twice(triple(quadruple(x))) == quadruple(twice(triple(x)))
Because these are equal, it conforms to associativity.
Note: The LEGO® analogy helps simplify the understanding of the associativity property too. Imagine you have three different LEGO® bricks you call A, B and C. If you attach A and B first and then C, you get a component that is exactly the same as what you’d get by attaching B and C first and then A. What you get is basically another LEGO® component you can use like the others.
Identity
Identity is the last rule, but it’s no less important than the other two. Consider the smiling diagram in Figure 2.8:
The identity property says that every object in a category must have at least one morphism to itself. This is why, in Figure 2.8, you have:
-
The objects
a
andb
. -
A morphism
f
froma
tob
. -
A morphism
ia
froma
to itself. -
A morphism
ib
fromb
to itself.
This must be true for all the objects in the category.
An example of ia
might be timesOne
or { x * 1 }
:
timesOne(x) == x
It’s interesting to use the identity with the previous properties. You can easily prove that, in a category, the following equivalence is true:
Note: Understanding why a category needs identity might not be very intuitive, and there’s not a plausible way to visualize identities using LEGO®. If a morphism in this analogy means to attach a LEGO® brick to another, it’s quite difficult to represent how to attach a piece to itself. On the other hand, you could think of the inverse of attaching two LEGO® pieces as the action of detaching them. In this case, the composition of attaching and detaching leads you to the initial piece.
The concept of isomorphism at the end of this chapter will probably help, but don’t worry — everything will be clearer when you get to Chapter 11, “Functors”, and Chapter 12, “Monoids & Semigroups”.
Now that you know what a category is, it’s time for some fun — you’ll give some meaning to objects and morphisms. Always remember that what’s true for a category will also be true when you give objects and morphisms specific meanings.
Category and logic
As mentioned, a category is a very abstract concept, but giving objects and morphisms some specific meanings makes everything closer to what you use every day.
In the context of logic, assume that objects are propositions and morphisms are entailments. Consider, then, Figure 2.10:
Using the symbol ⇒ to represent entailment, you have:
- The propositions
A
,B
andC
. - An arrow from
A
toB
, meaning thatA
⇒B
. - Another arrow from
B
toC
, meaning thatB
⇒C
.
To prove it’s a category, you need to verify the three important rules:
- Composition
- Associativity
- Identity
It’s time to have some fun!
Proving composition
As you know, composition is the property that allows you to compose a morphism from A
to B
and one from B
to C
into a single morphism from A
to C
. In this case, if A
⇒ B
and B
⇒ C
, is it also true that A
⇒ C
? Try to use the following propositions:
-
A
= Alice drives to work every day. -
B
= Alice has a driver’s license. -
C
= Alice is at least 18 years old.
The fact that Alice drives to work every day entails she has a driver’s license. That Alice has a driver’s license entails she’s at least 18. You then need to prove the following: Is the fact that Alice drives to work every day entailing she’s at least 18 years old? This is true, and this proves composition.
Note: In this example, you’re assuming Alice is in a place where you need to be 18 years old to drive a car and vote. You might also object that this works just for the previous propositions. In this case, you have two options: You can just believe it or find a case where this isn’t true. :]
Proving associativity
To prove associativity, you need a new proposition like:
-
D
= Alice can vote.
In this case, referring to Figure 2.10, you can use the following entailments:
-
f
=A
⇒B
= Alice drives to work every day. ⇒ Alice has a driver’s license. -
g
=B
⇒C
= Alice has a driver’s license. ⇒ Alice is at least 18 years old. -
h
=C
⇒D
= Alice is at least 18 years old. ⇒ Alice can vote.
From the definition of category, to prove associativity, you need to prove that:
(h◦g)◦f = h◦(g◦f)
You can break it down like this:
-
(h◦g)
= Alice has a driver’s license. ⇒ Alice can vote. -
(g◦f)
= Alice drives to work every day. ⇒ Alice is at least 18 years old. -
(h◦g)◦f
= Alice drives to work every day. ⇒ Alice can vote. -
h◦(g◦f)
= Alice drives to work every day. ⇒ Alice can vote.
Which proves the hypothesis.
Proving identity
The final property to prove is very interesting and funny. In logic, you basically need to prove that for every proposition A
, you can say that A
⇒ A
. This is equivalent to saying that:
- Alice has a driver’s license. ⇒ Alice has a driver’s license.
This actually has a name: tautology. :] This proves that logic is a category, and you’ll use it to introduce two more crucial concepts: initial and terminal objects.
Category theory and the real world
Before introducing initial and terminal objects, it’s valuable to stop for a second and think about an important aspect of category theory. In the introduction for this chapter, you read that object-oriented programming allows you to model your code using objects, which might seem closer to what you see and interact with every day. Can you say the same thing about a category?
A category has composition as a fundamental property. You can even say that category theory is the science of composition. Isn’t decomposing concepts into smaller ones what you do every day? Humans’ brains continuously decompose concepts to make them simpler to understand and memorize, and then recompose them. This might seem somewhat philosophical, but it’s proof that category theory isn’t something completely unrelated to reality.
At this point, an example might help. Suppose somebody asks you to solve the following addition problem:
7 + 10
Of course, you answer 17
. When you do that, are you getting the result from your memory, or is your brain actually computing the addition of 7
with 10
? Frankly, it could be either. With this simple addition, your brain has probably memorized the answer somewhere and is giving it as the answer.
Now, imagine somebody asks you to solve the following subtraction problem:
42 - 8
In this case, you probably don’t have the answer memorized, so your brain needs to do some “computation”. Because it’s not an obvious answer, your brain might do something like this:
42 - 2 = 40
40 - (8-2) = 40 - 6 = 34
Putting it all together, you might mentally compute:
42 - 2 - (8 - 2) = 34
Your brain has decomposed the simple subtraction into multiple operations that are probably easier to calculate and then composed the results back into a single value. This is an example of composition!
Initial and terminal objects
You already learned that category theory explains everything in terms of objects and morphisms. Not all the objects and morphisms are the same, though. For instance, not all the objects are somehow connected with a morphism. For logic, this means that a proposition doesn’t necessarily entail all the others. For the same reason, not all the propositions are entailments of another.
Note: Using the LEGO® analogy, you represent this concept saying that not all the LEGO® pieces can be attached to any other piece.
To understand why this is, you need the definition of uniqueness. In this context, you can say that the morphism f
between the objects A
and B
is unique if any other morphism g
between the same objects cannot be different from f
. In short, if this happens, f
and g
must be equal.
With this definition in mind, you can define an initial object as an object with a unique outgoing morphism to every other object in the category. A terminal object is an object with a unique incoming morphism from any other object. Figure 2.11 gives an idea of these concepts:
Not all categories have initial and terminal objects but, if they do, they are unique. In logic, the initial object has the name False and the terminal object True.
Category properties have funny implications on these objects:
- Each object has at least one identity morphism. This means that what is false is false, and what is true is true.
- Because there’s always a morphism starting from the initial object to any other objects, there’s also a morphism from the initial object to the terminal one. This means that a false assumption entails everything. Therefore, “Tom has wings” entails “Tom can fly”, is a counterfactual implication.
You’re probably wondering what all this has to do with functional programming — and Kotlin.
The good news is that anything you see that’s true for a generic category is also true for a specific one. What’s true in logic is also true in programming when you give a specific meaning to objects and morphisms. It’s now time to be more pragmatic and start studying the most critical category for an engineer — spoiler alert — the category of types and functions.
Exercise 2.3: Can you prove that using
Set
s as objects and “is a subset of” as morphisms results in a category? In other words, a morphism from setA
to setB
would mean thatA
is a subset ofB
. In that case, what are the initial and terminal objects?Don’t forget to check out Appendix B for hints and solutions.
Category of types and functions
So far, you’ve learned what a category is, and you also had some fun with the category of propositions and entailments. That allowed you to introduce the properties of a category and define some significant concepts like initial and terminal objects. That’s all good — but this is a book about programming, and you need something more pragmatic. You basically need to answer the following questions:
- What happens if objects are types and morphisms are functions?
- What’s the meaning of composition, associativity and identity in the category of types and functions?
- What’s the meaning of initial and terminal objects?
In the following paragraphs, you’ll answer these questions using the Kotlin language, and you’ll have some revelations about some of the most important Kotlin standard types. Here, using Kotlin, you’ll:
- Prove that using types as objects and functions as morphisms, you define a category.
- See what initial and terminal objects mean when dealing with types and functions.
- Find out where the Kotlin types
Unit
andNothing
come from.
As mentioned, you’ll do this using Kotlin.
Do types and functions define a category?
As a first step, you need to prove that by using types as objects and functions as morphisms, what you get is actually a category. You need to prove:
- Composition
- Associativity
- Identity
Proving each of the category properties is also a good exercise to review some interesting Kotlin concepts.
In the material for this chapter, you’ll find the starter project with some empty files you’ll fill in along the way. Start by opening the Aliases.kt file and write the following definition:
typealias Fun<A, B> = (A) -> B
This is a type alias that represents all the functions from a type A
to B
. If A
and B
are two objects of the category of types and functions, Fun<A, B>
is a morphism.
This simple definition allows you to prove each of the properties for a category.
Proving composition
To prove composition, you need to prove that for any function f
from A
to B
and any function g
from B
to C
, there’s an equivalent function: g◦f
from A
to C
, which is the composition of the two.
This is nothing new to you because you’re probably composing functions every day. Consider, for instance, the following code you can write in the Main.kt file:
fun twice(a: Int): Int = a * 2 // 1
fun format(b: Int): String = "Result is $b" // 2
These are very simple functions that:
- Double the
Int
value it gets as input. The type oftwice
isFun<Int, Int>
. - Format the
Int
it gets as input to aString
. The type isFun<Int, String>
.
You can compose twice
and format
in a very simple way, like this:
fun formatAfterTwice(x: Int) = format(twice(x))
You can prove this by adding the formatAfterTwice
definition in the Main.kt file along with the following:
fun main() {
println(format(twice(37)))
println(formatAfterTwice(37))
}
When you run this code, you get the following output:
Result is 74
Result is 74
This is just an example, but proving that this works for any type and function requires something more.
Open the initially empty Category.kt file in the project for this chapter, and add the following definition:
inline infix fun <A, B, C> Fun<B, C>.after(crossinline f: Fun<A, B>): Fun<A, C> =
{ a: A ->
this(f(a)) // HERE
}
Note: In the previous code you use the Kotlin keywords
inline
,infix
andcrossinline
. In this case,infix
allows you to use a syntax likeg after f
instead ofg.after(f)
. Theinline
keyword, as you’ll see in Chapter 4, “Expression Evaluation, Laziness & More About Functions”, allows you to basically replace everyafter
invocation with the expression it represents. Usinginline
then requires the use ofcrossinline
for the input parameter,f
, in order to allow no-local returns from the functionf
itself.For a full description of these keywords, please refer to Kotlin Apprentice, which is the best place to start.
This is a code representation of the (g◦f)
notation you were using before, where g
represents this
and f
represents f
.
The definition of after
has many interesting things to note. It:
- Is a generic function of the parameters types
A
,B
andC
. - Creates an extension function for the
Fun<B, C>
type. - Uses the
infix
andinline
keywords. - Accepts a function
Fun<A, B>
as an input parameter and returns a functionFun<A, C>
as output.
Note: The last point asserts that
after
is a higher-order function because it accepts a function as an input parameter and returns a function as output. Don’t worry — you’ll learn about higher-order functions in Chapter 5, “Higher-Order Functions”.
The definition of after
looks more complicated than it actually is. Looking at its body, it does exactly what you’ve done with formatAfterTwice
but in a more generic way. It:
- Returns a function with an input parameter
a
of typeA
. - Uses the parameter
a
as input for the functionf
. - Passes the result of
f(a)
as an input parameter for the function you use as the receiver, which in this case has typeFun<B, C>
.
You can now use after
with the previous example. Just add the following code to main
in Main.kt with:
main() {
// ...
val f: Fun<Int, Int> = ::twice // 1
val g: Fun<Int, String> = ::format // 2
val formatTwice = g after f // 3
println(formatTwice(37)) // 4
// ...
}
Note: In the previous code, you used
::
to reference a function using its name without calling it. For instance,::twice
is a reference totwice
.
Here, you:
- Define
f
as a reference to::twice
of typeFun<Int, Int>
. - Initialize
g
as a reference to::format
of typeFun<Int, String>
. - Create
formatTwice
as a reference of typeFun<Int, String>
tog◦f
. - Invoke
formatTwice
, passing37
as a value.
Build and run main
, and you get the following additional output:
Result is 74
Exercise 2.4: In this section, you defined
after
, which allows you to write expressions like:val formatTwice = g after f
Can you write
compose
instead, which would allow you to implement the same expression as:val formatTwice = f compose g
Again, give it a try and check the challenge project and Appendix B to see how you did.
It’s fundamental to note here the fact that after
compiles is proof that composition works for every type A
, B
and C
and every function F<A, B>
and F<B, C>
.
Proving associativity
To prove that the category of types and functions follows the associativity property, you basically need to prove that:
(h after g) after f == h after (g after f)
Open Main.kt and add the following function:
fun length(s: String): Int = s.length
Note: Here, you defined
length
explicitly, but you could useString::length
instead.
It’s a simple function that returns the length of the String
you pass as an input parameter. Its type is Fun<String, Int>
.
In the same Main.kt file, add the following code in main
:
fun main() {
// ...
val h: Fun<String, Int> = ::length // 1
val leftSide: Fun<String, Int> = (h after g) after f // 2
val rightSide: Fun<String, Int> = h after (g after f) // 3
println(leftSide(37) == rightSide(37)) // 4
}
In this code, you:
- Define
h
as the reference tolength
as a function of typeFun<String, Int>
. - Create
leftSide
as the left side of the equation you want to prove. - Define
rightSide
as the right side of the equation you want to prove. - Check that the two members are equal.
When you run main
, you get the following additional output:
true
You might object again that this specific example doesn’t prove anything — and you’re right! What actually proves that associativity works for the category of types and functions is the successful compilation of after
.
This is because it means that, given the types A
, B
and C
and the functions f
and g
, you can always create a function that is their composition.
Another way to prove it is to replace the definition of after
with its implementation. In this case, the left side of the equation is:
(h after g) after f =
({ b: B -> h(g(b))}) after f =
{ a: A -> { h(g(f(a)))}}
The right side is:
h after (g after f) =
h after ({ a: A -> g(f(a))}) =
{ a: A -> { h(g(f(a)))}}
The two members are exactly the same.
Note: In the last proof, you actually applied fundamental tools you’ll learn about in detail in Chapter 3, “Functional Programming Concepts”.
Proving identity
What does it mean to prove identity for the category of types and functions? It means to prove that, for every type A
, there’s always at least one function of type Fun<A, A>
. To create such a function, open the Category.kt file and add this code:
fun <A> identity(value: A) = value
Although this function proves that identity exists, it’s important to mention that it’s not the only one. The function twice
you created earlier, for instance, is an identity function because of type Fun<A, A>
.
At this point, there’s something interesting to say about identity. As mentioned earlier, twice
is an example of a function that maps distinct values in the domain to distinct values in the range. This means that twice
has an inverse function you can call half
and define like this:
fun half(a: Int): Int = a / 2
But what does it mean to say that twice
is the inverse of half
? This means that:
half after twice = twice after half = identity
Note: In this case, if you half a value and then double it, you get the same value. The same is true if you first double and then halve it.
When you have a function and an inverse function, you say that the functions are isomorphisms. This definition gives a first reason for the existence of the identity property. Of course, this isn’t true for all the functions from a type A
to a type B
. Some functions don’t have an inverse.
Anyway, it’s noteworthy that an isomorphic function somehow makes identity obsolete because it would just be the composition of the function with its inverse.
Exercise 2.5: Can you write an example of an isomorphic function
f
and its inverseg
and prove they always compose toidentity
? When you’re done, look at the solution in Appendix B.
This concludes the proof that types and functions creates a category. What, then, is the meaning of starting and terminal objects for the category of types and functions?
Initial and terminal objects
At this point, it’s interesting to see what the meaning of initial and terminal object is in the category of types and functions.
The initial object
As you learned earlier, the starting point is an object with a unique morphism compared to all other objects in the category. With types and functions, it means that the initial point is a type you can use as input to a unique function to any other type. Said in other words, any function that you call with this initial type must always have the same result.
In Kotlin, this initial object is Nothing
. You might argue that you could always write a function from Int
to any other type, and this is true. The problem is that the function must be unique.
If Int
were a starting point, the following two different functions of type Fun<Int, String>
:
val f: Fun<Int, String> = { a: Int -> "2 * $a = ${2*a}"}
val g: Fun<Int, String> = { a: Int -> "$a * $a = ${a*a}"}}
Would be the same function, but they aren’t! Instead, for any type A
you define:
fun <A> absurd(a: Nothing): A = a as A
This function’s name is absurd
because, if you want to invoke it, you need a value of type Nothing
, which is impossible. IntelliJ gives you a hint for this:
Note: You might wonder why some of the functions have names like
absurd
and others are anonymous, likef
andg
in the last example. The reason is that anonymous functions cannot be generic.
You might try to invoke it like this, giving the Kotlin compiler some hint about the generic type, but the result would be the same.
More importantly, because absurd
is a function you can’t invoke, it never returns, and this makes it unique. Any other function starting from Nothing
to any other type A
would do exactly the same, so it’d be the same as absurd
.
The terminal object
In the previous section, you learned where the famous Nothing
Kotlin type comes from. In the category of logic, you also learned that the terminal object is the counterpart of the initial object. A terminal object, if it exists, is an object with a unique incoming morphism from all other objects. In other words, all functions that return this type will return the same object.
In the category of types and functions, this means a terminal object is a type output of a unique function accepting an input parameter of any other type, Nothing
included. In Kotlin, this is the Unit
type.
For any type A
, you can create the function:
fun <A> unit(a: A): Unit = Unit
Also, in this case, there are many significant things to note:
- The
unit
function is generic with the typeA
, and it always returns something you represent withUnit
. - For any type
A
, the functionunit
is unique. -
Unit
isn’t just a type; it’s also the only value of that type.
To disprove uniqueness, you might try to create the following function as a possible alternative. This wouldn’t work:
fun <A> unit2(a: A): Unit {
println("I'm different")
return Unit
}
At the beginning of the chapter, you learned that the concept of function isn’t strongly related to the concept of computation. A function is a way to map values in the domain to values in the range. In terms of mapping, unit
and unit2
are the same function.
Note:
unit2
is actually a bad function because it hides a side effect, which is another fundamental concept you’ll learn about in the next chapter.
The last point is also essential. You learned that with category theory, you can only use objects and morphisms. What does it mean to say that Unit
is the only value for the Unit
type? What does it mean that a
is a value of type A
? In general, what’s the relationship between the concept of type and the probably more familiar concept of set?
Types and sets
In the previous section, you learned some interesting properties of the category where objects are types and morphisms are functions. But what is a type? What do you mean when you define a variable like this?
var a: Int = 10
You usually read this as “a
is an Int
”, but what do you mean by Int
? If you think about this, Int
is just a name to represent the set of all the integer values. a
is of type Int
means that you can assign to a
only values that are in the set you call Int
.
Note: To be accurate,
Int
represents the set of all the possible integers that you can represent using 4 bytes, so the whole numbers between -2,147,483,648 (-2³¹) and 2,147,483,647 (2³¹-1).
In the same way, consider the following expression:
var s: String = "Hello"
In this case, you’re defining the variable s
of type String
, which is a way to represent the set of all possible String
s. Again, you can assign to s
only elements of the set you call String
.
Thinking in terms of sets makes things easier. Consider the function twice
that you’ve already met:
fun twice(a: Int): Int = a * 2
This is basically a way to map elements in the set of Int
to other elements in the same set.
The function format
is a way to map elements in the set of Int
to elements in the set of String
.
fun format(b: Int): String = "Result is $b"
The following image gives a more intuitive representation of the previous functions:
Figure 2.14 can be a bit misleading, though, because it represents relations between elements of two set
s, which in this case are both Int
. But what does it mean to be an element of a set? How can you represent this using just objects and morphisms?
Definition of element
As you learned earlier, objects in category theory are like dots; they cannot be decomposed. This also means the morphisms are the only tool you can use to distinguish one object from the others.
In particular, category theory introduces the concept of structure, which you define using the incoming morphism. Because of this, the initial object has no structure. The terminal object, on the other hand, has a very clear and unique structure because there’s exactly one and only one morphism from any other object. This property makes the terminal object unique.
Nobody said that a terminal object can’t have outgoing morphisms. On the contrary, from the terminal object, you might have many morphisms to a given object A
, like in Figure 2.15:
More importantly, you can give a different name to each morphism, like x
, y
or z
.
You need to understand what this means for the category of types and functions. This means that for a given type A
, there are many functions of type Fun<Unit,A>
, one for each value of type A
.
As a simple example, consider the type Int
. You can create a different function of each value of Int
, like these you can add to the Main.kt file:
fun one(u: Unit): Int = 1
fun two(u: Unit): Int = 2
fun minusThree(u: Unit): Int = -3
// ...
A function for each element of the set you associate to the type Int
and the name you give to that function is an element of the set A
represents.
To see how to describe a simple invocation of a function using composition, just add the following code to main
:
fun main() {
// ...
// twice 2
val twiceTwo = ::twice after ::two // 1
println(twiceTwo(Unit)) // 2
// ...
}
In that code, you:
- Define
twiceTwo
as the composition oftwo
andtwice
. - Invoke
twiceTwo
, passingUnit
as a parameter.
When you run that code, you’ll get the expected output:
4
Initial and terminal objects using sets
Thinking in terms of sets makes things a little bit easier. The initial object, by definition, doesn’t have any incoming morphisms. It’s the type for a set without any elements. Nothing
is like the empty set. If you consider the concept of subtype related to the concept of inheritance, you also understand why Nothing
is a subtype of every other type in Kotlin. This is because the empty set is a subset of every other set. If you look at the source code for the Nothing
type, you’ll find this:
public class Nothing private constructor()
Nothing
has a private constructor. This means that Nothing
is a type, but you can’t create any instances of it.
What about the terminal object? By definition, there’s a unique morphism from any other type. This means there’s a unique function from any other type. If you consider the terminal type to be a set, this means it’s a set containing a single value that you know, in Kotlin, has the name Unit
. Look at its source code, and you’ll find this:
object Unit {
override fun toString() = "kotlin.Unit"
}
This means that Unit
is a type, but it’s also the name for its unique instance.
Function types
In one of the previous paragraphs, you created the following definition:
typealias Fun<A, B> = (A) -> B
With Fun<A, B>
, you wanted to represent the set of all the functions from A
to B
.
According to what you learned previously, this is exactly the concept of type of a function. You’ve already learned how the category of types and functions works. If the objects of that category are types of functions, what would the morphisms be? This is something you’ll learn in the following chapter, and in particular, with the concept of functor.
Challenges
In this chapter, you learned some fundamental concepts about category theory and functional programming. It’s now time to solve some challenges and have some fun. You’ll find the solutions in Appendix B, and the code in the challenge project for this chapter.
Challenge 1: Functions and sets
How would you represent a specific Set
using a function? For instance, how would you represent the set of even numbers with a function? After that, how would you print all the values in the set?
Challenge 2: Functions and sets again
How would you represent the intersection and union of two sets using functions? The intersection is the set of objects that belong to set A and set B, and the union is the set of all objects that belong to set A or set B.
Challenge 3: The right domain
Consider the following function:
fun oneOver(x: Int): Double = 1.0 / x
What’s the domain and the range for this function? If you invoke oneOver(0)
, you get an exception. How can you be sure you only pass values in the domain as an input parameter?
Key points
- A function is a way to map things from a domain to things in a range.
- Category theory is necessary for understanding the fundamental concepts of functional programming.
- You define a category using objects and morphisms, which must follow the fundamental rules of composition, associativity and identity.
- Logic is a category that makes some concepts closer to the way humans think.
- The category of types and functions is the most important for a software engineer because it explains functional programming concepts.
- The initial object in a category has outgoing unique morphisms to all other objects.
- The terminal object in a category has incoming unique morphisms from all other objects.
- Not all categories have a terminal object.
- Initial and terminal objects explain the meaning of the Kotlin standard types
Nothing
andUnit
. - It’s useful to think of a type for a variable as a way to represent the set of all the values that variable can reference.
- Understanding the relationship between types and sets simplifies some of the most critical functional programming concepts.
Where to go from here?
Congratulations! At this point, you have an idea of what a category is and why category theory is important in understanding functional programming. It might have been tough, but you don’t have to worry if something isn’t completely clear at this point. In the following chapters, you’ll have the opportunity to see these concepts again in a more practical context. In the next chapter, you’ll start to focus on pure functions.
Note: The inspiration for this chapter comes from the excellent work of Bartosz Milewski in his YouTube video series Category Theory for Programmers.