Programming with Categories - Lecture 8

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

[michaeldurig]

This is a brilliant introduction to adjunctions from Brendan!

[naayou]

minute 26:00ish regarding the origin of the Currying, the conception goes back to Schönfinkel. Haskell B. Curry used it extensively in his work. The association of the term with Curry is mainly due to Strachey.

[eastquack]

I have a feeling that the pace is double time; I think that Bartosz's vids are more sensibly paced

[SawmonandNatalie]

00:11:13 𝗍𝗒𝗉𝖾 𝖭𝖺𝗍 𝖿 𝗀 = 𝖿𝗈𝗋𝖺𝗅𝗅 𝖺. 𝖿 𝖺 -> 𝗀 𝖺
00:19:48 both *[ ]* and *Maybe* functors map category of Haskell types into two proper full sub-categories of it. There is a natural transformation between these two sub-categories given by *safeHead* .

[zackKenyon]

I'm pretty confused as to what object \alpha_{a, c} is suppoed to be. C and A are diferent categories, so I assume it's actually the functor R acting on some chosen element of C(La, c)?

[tkjyxrb]

So for CCC we can go from C(a, c^b) via -xb to C(axb, (c^b)xb) then via eval to C(axb, c), but how to return?
From C(axb, c) via -^b to C((axb)^b, c^b). Now, how to get rid of exponentials?

[mathandemotion]

The second half seriously fucked me up. Anybody know of an explanation for the final task, proving naturality of eval? I got as far as saying "Well, if the functor on the left (_^b x b) only applies lifted morphisms to the _, then for morphisms eval is just the identity", but can I make that assumption? (Am I even using the right terminology?)

Basically, tell me how this is wrong:

(c^bxb) -> c
|
(_xb) (_^b) f
v
((f c)^b x b) -> f c

With the right downwards arrow reading just f.

[inakiesparza]

Brensan is very intelligent, but I think he is not very good at teaching. Too nervous and too fast,

[michaelkohlhaas]

Lecture 8 and we are talking about safeHead! Wow! Frigging boring!