Programming with Categories - Lecture 6

Lecturers: Brendan Fong, Bartosz Milewski, David Spivak

Summary: In this course we explain how category theory—a branch of mathematics known for its ability to organize the key abstractions that structure much of the mathematical universe—has become useful for writing elegant and maintainable code. In particular, we'll use examples from the Haskell programming language to motivate category-theoretic constructs, and then explain these constructs from a more abstract and inclusive viewpoint. Hands-on programming exercises will be used to demonstrate categorical ideas like "the universal property of products" in working Haskell code.

We will assume no background knowledge on behalf of the student, starting from scratch on both the programming and mathematics.

(Video: Paolo Perrone.)

[SawmonandNatalie]

00:16:03 *Terminal* type in Haskell
00:24:10 *Initial* type or *Void*
00:39:45 *product* // 𝖽𝖺𝗍𝖺 𝖯𝖺𝗂𝗋 𝖺 𝖻 = 𝖯𝖺𝗂𝗋 𝖺 𝖻 ...

[bblfish]

Note that point free notation is a bit of a weird name, because the point free notation is exactly the one that uses points. What is meant of course is that one does not use a point in the set.

[bblfish]

The answer to the question around min 26 about how Void compares to the Nothing in Maybe, is I think that Nothing is isomorphic to Unit. In Category Theory Maybe(X) = 1+X (ie 1 or X). So there definitely is an element of 1. It's just that when we have that 1, we don't have X (which is why it has the slightly confusing name Nothing).

[knowledge]

34:52 Brendon departs with questions: what are the products the categories examples B and Div(30. Ar the answers F and 5, respectively? In general, is the join (least upper bound)?

[balthazarbeutelwolf]

Slight issue: in Haskell, this is not quite a product, because Haskell is lazy - and for similar reasons the () type is not terminal in Haskell either (void is though). To construct a proper product in Haskell one needs to make the MkPair constructor strict in both arguments, via a !-annotation. In that setting MkPair undefined undefined is indistinguishable from undefined.

[EugeneCrosser]

What does it mean that in Boolean category there is an arrow from False to True, but no arrow back? He said "False implies True, but not the other way around". Why is it so?

[paultaylor]

In the terminal object definition are 2, 3 and 5 also terminals? In fact are they not all terminals since there is one morphism from every object which is divides into which is the very thing that defines the category.

[cataclysmwarshulduar]

If there are 2 terminal objects A and B, then there must exist morphisms F : A -> B and F2 : B -> A. They are therefore isomorphic
Is this good enough?

[matthiasasemota]

I don't like the fact that Bartosz felt so rushed...