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

- All Categories 2.3K
- Chat 494
- ACT Study Group 5
- Azimuth Math Review 6
- MIT 2020: Programming with Categories 53
- MIT 2020: Lectures 21
- MIT 2020: Exercises 25
- MIT 2019: Applied Category Theory 339
- MIT 2019: Lectures 79
- MIT 2019: Exercises 149
- MIT 2019: Chat 50
- UCR ACT Seminar 4
- General 64
- Azimuth Code Project 110
- Drafts 1
- Math Syntax Demos 15
- Wiki - Latest Changes 1
- Strategy 110
- Azimuth Project 1.1K

Options

*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.

## Comments

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 fidefunctor.<END-TALK/OPEN-DISCUSSION>

`_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>`

Exercise: Prove that the polymorphic type constructor:

is a functor taking Hask to Hask. (Again, simplified, "Platonic" Hask.)

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