6.2: Functors in programming | Categories Bartosz Milewski Youtube notes

The `Maybe` functor, continued

We have defined the mappings of the Maybe functor (see previous video) but we still need to see if it respects the additional conditions, sometmes calles functor laws : it must preserves identity and composition.
In Haskell, the compiler cannot check, the type system cannot encode these conditions. However, unlike in other languages, there is a way of using Haskell on a black or white board to formally prove things about the language.
In Haskell, every definition af a function is an equality : "this function acting on this argument equals this expression". It's an equation that permits to replace the left side by the right side whenever we find it in a program, which is called inilining. Inlining is not always correct if it has side effects, like in C or C++ macros. But in Haskell, functions are pure and inlining can be done safely. And we can do the opposite of inilining : refactoring, replacing an expression by a function call. In Haskell, this is guaranteed to work.
This can be used to do equational reasoning. If we can show, using inlining and refactoring, that we can go from a result to an other, then these two things are equivalent.

Identity

We need to prove that

fmap id_a = id_{Maybe a}

But it's a polymorphic id, it's defined for every type by the same formula (parametric polymorphism), so we can write :

fmap id = id

fmap and id are already defined, so we just say "these two functions are equal", which means that they have equal values on equal arguments.
Equational reasoning : when fmap acts on id, it produces a function from Maybe a to Maybe a. So two cases to check : this maybe could be a Nothing or a Just.

fmap id acting on Nothing. By definition of fmap, fmap Nothing = Nothing.
And the definition if id is : id x = x.
So Nothing = id Nothing (this is refactoring).
So fmap id Nothing = Id Nothing
fmap id acting on Just x. By definition of fmap, fmap id(Just x) = Just (f x)
So fmap id(Just x) = Just(Id x) = Just x
And by definition of id, id(Just x) = Just x
So fmap id(Just x) = Just x

Composition

We need to prove that

fmap(g . f) = fmap g . fmap f

Corresponds to this diagram :

(TODO : add fmap g . fmap f)

This can be showed by equational reasoning using the same method as we did for identity (It's done on the blog page about functors).
Strictly speaking there is no need to prove it because as we use parametric polymorphism, this is a theorem for free. Once the id property is proven, this follows.

Functors in Haskell

Let's see how to define a functor in general in Haskell. It's called lifting (the functions obtained by a functor are "above" the original ones in the figure. Lifting in Haskell

fmap is a higer-order polymorphic function ; higer-order because it takes a function and produces a function ; polymorphic because a and b are arbitrary types. A different fmap is defined for every functor, with different implementations. We have an example of ad'hoc polymorphism ; depending on the parameter (the functor in this case), the implementation of the function (fmap in this case).
We use type class : a family (class) of types that share a common interface. In Haskell, for example a class that supports equality :

class Eq a where
    (==) :: a → a → a Bool;

Some type a is a member of Eq class. operator == takes two a and produces a Bool, meaning : "is the first a equal to the second one ?" (yes or no). One name for the function (==) will serve for many different types. The implementation will be different for every type.
But functors are not parametrized by type, functors are type constructors. In Haskell, the class mechanism works equally well for type, type constructors and more exotic things.
The to define a fnuctor in Haskell, we write

class Functor f where
    fmap :: (a, b) → (f a → f b)

The compiler knows it's a type constructor because f acts on a type to produce an other type, so f is a type constructor.
Because of currying (we'll see later), parentheses can be skipped and write

class Functor f where
    fmap :: (a, b) → f a → f b

The `List` functor

data List a = Nil | Cons a List(a)

A list of a is either empty or consists of a head of type a and a tail.
List is a type constructor ; it takes an arbitrary type and creates a list of this type.
Is is a functor ? Obviously yes because it's built algebraic data types. But we don't know that yet, so let's define its function fmap.

instance List Functor where
    fmap _ Nil = Nil
    fmap f(Cons h t) = Cons((f h) (fmap f t))

List is an instance of class Functor ; providing the implementation of fmap proves that it's a functor.
fmap takes a function from a to b and produces a function from List a to List b.
fmap _ Nil = Nil : an empty list produces an empty list (the underscore replaces f when f is not used in the right part of the equality).
fmap f(Cons h t) : h (head) is of type a ; t (tail) is of type List a. The recursive call to fmap will act on the tail.

The `Reader` functor

type Reader ra = r → a

The type constructs the arrow itself.
It could be expressed as

type Reader ra = (→) r a

It is like a type constructor but it takes two types as arguments, r and a and produces a type of function from r to a.
So far we've seen constructors that take one type as argument, but here it takes two types. But we can always fix one type and only care about the second one.
So we fix r, fix the arrow and vary only a.
The Reader r functor a mapping between type a and a function from r to a.
This is called currying or partial application : you have a function of two arguments, you fix one argument and it becomes a function of one argument.
The fmap function of Reader :

fmap :: (a → b) → (r → a) → (r → b )

fmap f g = f o g = (.) f g

fmap = (.)

Intuition behind functors

(For endofunctors)
There are also the Const, or Identity functors. They all seem totally different.
The intuition is that when a functor is acting on some type, it encapsulates the values of this type, somehow hides them.
An element of the type "functor of a sort of has elements of type a in it.
So we can think of a functor as a container.
This is obvious for some functors, like List, Tree, Vector.
Some functors seem more problematic, like Maybe, which contains either nothing (empty container) or an a.

Applying a function to a container means opening it and applying the function to the contents.

Can we see Reader as a container ? For example if a is a boolean, a function taking a bool as argument can return two values ; in this sense it "contains" a boolean, this is even more understandable if we memoize the function

The distinction of a data type and a function is weak.
For axample in Haskell, a list from 1 to infinity [1 ..] ; this is data but this can't be stored into memory an internally it is implemented as a function which produces the elements on demand.
A function is a data, a data is a function. We'll see that a function type is in category theory is actually an exponential, which is a data type.

In C++ there is something called future which contains a value to be evaluated by an other thread ; it may contain or not a value, depending if it's already evaluated. And you can apply a function to this value wether it is evaluated yet or not.

The only important thing about a functor is that you can apply a function to what it contains. A functor doesn't give you a way of retrieving this value, it is not part of its definition.

The Maybe functor, continued