"Categories for the Working Hacker" by Philip Wadler

The talk will explain why category theory is of interest for developers, taking examples from Java and Haskell, and referencing the new blockchain scripting languages Simplicity, Michelson, and Plutus. The principle of Propositions as Types describes a correspondence between, on the one hand, propositions and proofs in logic, and, on the other, types and programs in computing. And, on the third hand, we have category theory! Assuming only high school maths, the talk will explain how categories model three basic data types: products (logical and), sums (logical or), and functions (logical implication). And it explains why you already learned the most important stuff in high school.
Speaker: Philip Wadler

[@carterthaxton]

This guy is amazing. I’ve learned as much about how to give a great presentation as I have about category theory. Thank you!

[@bilalf]

> "Object oriented programming" is really well named. You should just object"

[@CubOfJudahsLion]

They should make Wadler give *every* computing talk ever.

[@ymi_yugy3133]

I am really impressed. This is the best introduction to category theory and thinking about known structures in terms of universal properties I've seen yet.

[@jamma246]

I didn't know that Philip Wadler gave such entertaining talks, really enjoyed that!

[@mikkolukas]

28:46 the example is missing a closing '}' just after the return statement.

[@bibliusz777]

didn't expect this guy to mention Plutus

[@cryptonative]

“That is what Category Theory is all about- avoiding traffic jam”. It just clicked

[@gilbertg.96]

I wish you were my math teacher.

[@sendark001]

he was my informatics professor at uni. His was the only 9am lecture that was full in the whole campus :)

[@ARVash]

plfa.inf.ed.ac.uk so you don't have to type

[@MrGoatflakes]

dead link ;/

[@mskiptr]

Now a redirection to plfa.github.io/

[@a13ph0]

it's alive! alive!

[@imode256]

So, my question is that if a category corresponds to a proof fragment (logical connective), can I string together proof fragments to get a proof? If so, wouldn't that mean that, in the categorical view of things, computation corresponds to graph reduction because computation corresponds to proof simplification?

[@alonzoc537]

Yes. That is all... Nah just kidding, if you are interested in this view of computation you should look at citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.90.2386 (An algorithm for optimal lambda calculus reduction). Which shows how lambda calculus can be evaluated using a graph reduction algorithm (And in an optimal way at that. Plus if you built a runtime on this concept you could get multi-threading for free!).

[@kernalphage]

FP is pretty new to me, let me see if I understand this: Products allows you to take 2 types and 'expand' them into a single type? Giving you a type that is all possible combinations of two Enums, for example. While sums lets you "condense" down 2 things (A and B) into 1 (C)? And for some Sums to be useful, (A and/or B) and C should be the same type? So you can do stuff like (ErrorInt => ErrorInt) => ErrorInt or (ErrorInt => Int) => ErrorInt? I know it's tradition to use the same symbols in the diagrams and in the example code, but I think using and [Left, Right] everywhere instead of concrete types is making it really hard to reason about places I'd use these kinds of constructs. Even using something like Alice/Bob/Coworkers might be helpful, and you can go more abstract from there.

[@daweiliu6452]

Which text book do people recommend to learn Category theory?

[@JohnCook]

Steve Awodey's book Category Theory is popular.

[@Omega0202]

Category Theory for Programmers is good, it is free, and it has piggies: bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/

[@Yetipfote]

"Would you like to see it in Java?" *half the audience packs their suit case*

[@ittixen]

There was an undeniable vocal *noooo* from a significant portion of the audience.

[@qwertyman1511]

24:00 why is the case of double false excluded? aka, an Option that is Null, rather than [Result x / None]

[@NormanVN]

In logic, statements which are false are not 'valid statements'. You can say "2 is even" and it be valid, you can say " '3 is even' is false" (in plainer english: 3 is not even) and be a valid statement. But it's invalid and not a permitted statement to say "3 is even". That statement is not possible to construct from valid statements. So if you have a valid option of String/Integer, it either contains a string or an integer. It's possible to have a type which is either something or null, but that type is an option between something and the null token. It's also valid to have a type that's an int, a string, or null.

[@123TeeMee]

What does the dotted arrow actually mean?

[@alexeykrylov9995]

That there exists exactly one such arrow satisfying this diagram (that is, commutativity conditions in the diagram) given non-dotted arrows.

[@johnmorrison2645]

Java now has records.

[@JixuanLIU]

It's missing in his example of the sum, what to do if the left is an error and the right is an error too?

[@markzaidelman]

"Right" in his example represents a correct calculation, never an error. You can name the type differently: "Sum a b = Error a | Correct b". Hope that makes it more clear.

[@waltermays5551]

I assume you are talking about the first and second arguments? In that case, it will match the first pattern (f (Left e) _) and execute that code.

[@mattetis]

Doesnt that just mean that you have a sum that represents two different classes of errors? Edit: Something like type GenericError = SegmentationError + AccessError And your function can now switch over the two types summed in the more generic type

[@epgui]

Is the "omega" in "F omega" just another word for a functor? That's what it sounds like, but it wasn't said.

[@ee_color]

So we have sum, product and exponential. I wonder what subtraction, division and square root is.

[@jonaskoelker]

That's a good question. The two ideas underlying your question are, I think, that (a) the first set of operations (sum, product, exponential) all have inverses; and (b) when we reuse a name (sum etc.) in a new context, it should behave roughly as it did in the old context. For example, when we use the name "+" for string concatenation, we expect it to be associative (it is, e.g. ("hello"+"lovely")+"world" = "hello"+("lovely"+"world")), to have a neutral value that acts like 0 (it has: the empty string, as ""+x equals x for all x) and to have an opposite, string subtraction (it doesn't, really, but maybe the other properties are "the same enough" that "+" is non-confusing). I think in the context of categories, sum and product as defined in this talk are the opposites of each other: if you look at the diagrams (at 10:20 and 20:35), you'll notice that if you reverse the arrows in one diagram it should look like the other diagram. (They have different names including vs. [], but it's the structure that makes diagrams "scary-equals" :D i.e. equivalent for some value of equivalent, which might be category isomorphism but that's beyond my already limited knowledge.)

[@milanstevic8424]

I think that would be a logical inverse. I.e. with a sum and product you add something to the table, while subtraction and division, in my mind at least, would have to take something from the table, meaning that the operands should be logically negative. In that sense, the diagrams are the same, but the sets are inverse. So a division of apple and orange would be a pair of something that doesn't have an apple but doesn't have an orange either. I don't know if it's mathematically valid, it's just my intuition. But that would explain why it isn't particularly useful in isolation. Instead of thinking and talking about such a division, it is much more fruitful (pun intended) to talk about the actual product.

[@Arbmosal]

In general operations don't have inverses. E. G. In the natural numbers we don't have subtraction, in integers no division in rationales no roots

[@mattetis]

Wouldnt a "negative" sum type be a sum type with some set of values ommitted instead of added to it? If "-" would be our "type subtraction", "number" the type for natural numbers, and "0" the type that contains only the value 0 We could do something like: type NumberWithout0 = number - 0 To "subtract" 0 from the number type

[@Omnifarious0]

A+B seems more like xor, not or.

[@ccreutzig]

Imagine A and B being sets, and C = {true, false}. Obviously, we call those a true for which f(a) = true etc. What is the set of things in A+B that has (ab) = true? Everything true from A plus everything true from B.

[@MindcraftMax]

Well, it really is neither. It is a _disjoint_ union, which means elements of both type A and type B are still counted twice in A+B. So for instance A+A has twice the number of elements in A, whereas A _or_ A equals A, A _xor_ A equals empty type (since TRUE _xor_ TRUE is FALSE and not double TRUE as in the disjoint union).

[@J4j4yd3r]

logical or, not binary or. So yeah, exclusive vs inclusive or.

[@anilraghu8687]

Curry Howard Correspondence.