#### Howdy, Stranger!

It looks like you're new here. If you want to get involved, click one of these buttons!

Options

# [section4] 1.3 - Maybe as a functor

edited March 3

The idea of Maybe as a functor.

We've seen that the polymorphic type constructor "Maybe a," which maps a type to its maybe-ification, acts as a function from Haskell types to Haskell types.

Now let's picture the collection of Haskell types as a category, where the objects are types, and the morphisms are functions from one type to another. The name given to this category is "Hask."

Note: there are complications that arise from functions which don't terminate. At this early stage in the development, we'll simplify the picture, and limit our consideration to Haskell functions which always terminate (total functions). The category of Haskell types and total Haskell functions is called "Platonic Hask." In this context, when we write Hask will implicitly mean Platonic Hask.

Can we construe Maybe as a functor, where Maybe: Hask -> Hask?

We've already seen that the type constructor "Maybe," which maps the type a to Maybe a, gives the object portion of a functor.

What's left is to define the morphism component of a functor with Maybe, and then to show that this would-be functor satisfies all the functor requirements.

So, suppose "a" and "b" are types, and "f" is a morphism -- which means a function, in the setting of Hask -- from "a" to "b". That is, "f: a -> b".

In order for Maybe to be a functor, we need to define Maybe(f): Maybe(a) -> Maybe(b).

This is called the "lifting" of the function f, by the functor Maybe, to a function Maybe(f).

There's only one thing that f' = Maybe(f) could possibly be.

Choose x in Maybe(a). We must now define f'(x), which must be a value in Maybe(b).

We proceed by case, on the form of the constructor that was used to build x.

Case 1: x = Nothing.

Now there's nothing else besides Nothing that f'(Nothing) could possibly be.

Recap: (Maybe(f))(Nothing) = f'(Nothing) = Nothing.

Case 2: x = Just(y). Now we have to define f'(x) = f'(Just(y)) as some value in Maybe(b).

Now the lowest-hanging-fruit functor in this setting is the one which maps like things to like things. So Just(y) will be expected to map to Just(y'), for some value y' in b.

So, how are we going to come up with a y' in b? Let's look at what we've got to work with, the gives: a value x in a, and a function f: a -> b. Then to get a value y' in b, we simply apply the function f to x. So Just(x) will map to Just(f(x)).

That's it, our hand was forced all along the way.

Recap:

(Maybe(f))(Nothing) = f'(Nothing) = Nothing
(Maybe(f))(x) = f'(x) = Just(f(x))

That's our candidate functor.

To confirm the functor for office, we must next prove that it satisfies its oaths, which are the functor laws.

This is more of a clerical exercise, which we'll take care of in the following appendix.

• Options
1.
edited January 31

Appendix: Proving that Maybe is definitely a functor.

Time to dot our i's and cross our t's.

We've defined two functions:

Now to show that it's a functor, we need to prove: it maps the endpoints of arrows correctly, it preserves identities, and it respects compositions.

We already showed endpoint preservation: Maybe(f: a -> b): Maybe(a) -> Maybe(b).

Next, let's prove the identity law.

Maybe(id_A)(Nothing) = Nothing Maybe(id_A)(Just(x)) = Just(id_A(x)) = Just(x)

This shows what we needed: $$Maybe(id_A$$) = $$id_{Maybe(A))}$$

Now suppose f: a -> b, g: b -> c.

Then g . f: a -> c.

Maybe(g . f): Maybe(a) -> Maybe(c).

Maybe(g . f)(Nothing) = Nothing

Maybe(g . f)(Just(x)) = Just((g . f)(x)) = Just(g(f(x)) = Maybe(g)(Maybe(f)(Just(x))).

Hence, Maybe(g . f) = Maybe(g) . Maybe(f).

That's it, we've proven that Maybe is a bona fide functor.

<END-TALK/OPEN-DISCUSSION>

Comment Source:_Appendix: Proving that Maybe is definitely a functor._ Time to dot our i's and cross our t's. We've defined two functions: Maybe: Ob(Hask) -> Ob(Hask) Maybe: Arrows(Hask) -> Arrows(Hask) Now to show that it's a functor, we need to prove: it maps the endpoints of arrows correctly, it preserves identities, and it respects compositions. We already showed endpoint preservation: Maybe(f: a -> b): Maybe(a) -> Maybe(b). Next, let's prove the identity law. Maybe(id_A)(Nothing) = Nothing Maybe(id_A)(Just(x)) = Just(id_A(x)) = Just(x) This shows what we needed: \$$Maybe(id_A\$$) = \$$id_{Maybe(A))}\$$ Now suppose f: a -> b, g: b -> c. Then g . f: a -> c. Maybe(g . f): Maybe(a) -> Maybe(c). Maybe(g . f)(Nothing) = Nothing Maybe(g . f)(Just(x)) = Just((g . f)(x)) = Just(g(f(x)) = Maybe(g)(Maybe(f)(Just(x))). Hence, Maybe(g . f) = Maybe(g) . Maybe(f). That's it, we've proven that Maybe is a _bona fide_ functor. <END-TALK/OPEN-DISCUSSION>
• Options
2.

Exercise: Prove that the polymorphic type constructor:

Identity a = MkId a


Comment Source:Exercise: Prove that the polymorphic type constructor: ~~~ Identity a = MkId a ~~~ is a functor taking Hask to Hask. (Again, simplified, "Platonic" Hask.)