Category Theory 8.2: Type algebra, Curry-Howard-Lambek isomorphism

Type algebra, Curry-Howard-Lambek isomorphism

[@spastikxchild13]

Is it just me, or is anyone else's mind fucking blown?

[@fourZerglings]

When I saw conjunction and disjunction, I was wondering what NOT will map to. So for anyone interested: you can derive NOT from AND, OR and implication. A => B is equivalent to !A or B. If we replace B with false, we get just !A. Corresponding thing in categories is a -> Void (the set of functions mapping a to empty set). Indeed, if a is an empty set, there exists single morphism, Void -> Void, which is identity of Void. If on ther other hand a is not empty, there can be no morphisms from a to Void, because a function must return something, and it can't.

[@jakubdubovsky6081]

I like how "False => True" proposition corresponds to existence of Absurd function!

[@elias_toivanen]

Jakub Dubovský ex falso quod libet 🙂

[@kahnfatman]

Mathematicians are really really really fantastically absurd... and somehow we need them.

[@MithicSpirit]

not necessarily, since it also corresponds to the existence of the "unit" function (a -> (), which is the same as any => True).

[@TheDickswab]

Can't wait for the natural transformation lectures!

[@laagislaag]

This series is just absolutely amazing. Thank you!

[@uldir]

Thank you so much for your lectures! i am a maths teacher learning programmation (C++, Java, Python mainly) for 6 months only, and its because lessons like this i get interested in computer science. Its very beautiful to see connections between maths and other sciences, for example 2:50 "currying!..." i dont know what is "currying" but i know the adjoint fonctor isomorphism^^ Hom(A, Hom(B, C)) = Hom( A Tens B, C) i m sure all is in eilenberg-McLane homological algebra even if im far from this level, but i always had the intuition that 21century maths began with Poincaré algebraic topology, then Grothendieck and other, until now Homotopy type theory, this are fascinating subjects. I have always searched for clear courses on the subjects but always too hard. You explain the best way imo and scientific should always have the passion. And im not surprised you come from physics.

[@constipatedlecher]

0^0 is a great example too. In ordinary arithmetic it's undefined, but category theory gives you a pretty legitimate argument that if one were to define it, they'd have to define it to be 1. Also - the nth root function is a good example too; it corresponds to function application.

[@Alkis05]

There is a pratical reason for not defining 0**0 to 1. For example, the lim (exp(-1/x)**sin(0) = 1/e when x→0+, even though (sin(x), exp(-1/x)) → (0,0) when x→0+. But if you enter exp(-1/0)**sin(0) in ghci, you get 1. Why, because they evaluate each function separately, and since 0**0 is defined to 1, we don't get the correct result, that should be 1/e. If you enter x=0.01 it gets close to 1/e, drops to 0 when x=0.001 and back to 1 when x=0. That is a problem.

[@Erkkasieni]

At least, there is a reason to not define it as 0. Anything else goes, right?

[@MithicSpirit]

@@Alkis05 that logic only applies if the function is continuous at that point, that is, lim x->a f(x) = f(a), which doesn't have to be the case. In this specific case, where f((b,p)) = b^p and a = (0,0), the limit doesn't even exist since different paths through R² approach different values, so the function is definitely not continuous at (0,0) and hence your argument doesn't apply.

[@soufianemgInk]

I can't thank you enough for this amazing course

[@SisypheanRoller]

The analogy between Either and logical disjunction got me thinking. In a disjunction, we must have at least one of its propositions true: this allows the case where both are true. However, Either (in Haskell) can only be Left/Right but not both. This is fine since it tracks the disjunction's requirement of "at least one true", but it seems to suggest that you end up with a product (Left err, Right res) in the event that you get both true and you want to preserve that in your execution. I had a good chuckle trying to imagine scenarios where you might end up with a computation that failed AND succeeded. Of course, I assumed that Left corresponds to an error, which need not be the case. Interesting to think about nonetheless. I'm learning so much from these lectures it's super addicting. Thanks for putting these on KZbin!

[@edgardavid1653]

Wow! Loved the explanation. I'm getting familiar with Montague semantics and categorial grammar and this short lecture made such a complex topic (from my perspective at least) quite clear and digestible. thanks a million

[@rakittna90]

Are unique pointers in C++ really example of linear types? As far as I have understood linear types are only possible in total languages as you can always leak and bypass use-atleast-once requirement (Now that I think about it, wouldn't linear types be impossible in any language that has bottom type). And yes rust is pretty much build on affine types (avid rust user here :P). By the way these lectures are the best resource for category theory that I have found thus far. Thanks for making them and publishing them for everyone to see!

[@kingyinyan254]

Thanks, this is very helpful, in particular the "-Lambek" part :)

[@hassaannaeem4374]

great vid!

[@MarcelloDelBuono]

I understand better the first lecture now. And I wonder: is it possible to formulate classical mechanics as a category? If yes, that would show that the way human think mirrors the macroscopic reality they experience every day.

[@haribageski3327]

I enjoyed the lecture very much. I have one unclear thing, I thought Either represents exclusive disjunction, not disjunction?

[@stanisawbarzowski6706]

It corresponds to a (regular) disjunction. Example: both Bool and Int have elements. Either Bool Int obviously also has elements, for example Left True or Right 42. And we only care about whether it has any elements at all.

[@DrBartosz]

No, it's not exclusive. For instance, you can have Either Int Int, and it is not empty.

[@constipatedlecher]

I think you're probably confused because in some fields, the + with the circle around is used for XOR, while in others, it's used for coproduct (like in algebras, from abstract algebra).

[@Vinje92]

17:50 We called it sum, right?

[@dmvaldman]

What is the equivalent of ~a (not a)?

[@constipatedlecher]

Functions from a to the initial object (empty set). Think about it -- the only set that has a morphism to the empty set from it *is* the empty set! So if you're saying that a -> empty *is* inhabited, that's the same as saying that a is *not* inhabited.

[@Alkis05]

​@@constipatedlecher But what if a is void? If a is false, the proposition is true. So Void -> Void is equivalent to { a } ? Am I missing something?

[@constipatedlecher]

@@Alkis05 Yes, Void -> Void is equivalent to the set with one element. There is exactly one element of Void -> Void; it is the "empty function" that assigns no elements to no elements. In many (most?) presentations of classical logic, ~a is actually syntactic sugar for a -> False.

[@Alkis05]

@@constipatedlecher "Void -> Void is equivalent to the set with one element" Right, I was looking at the "emptiness of the objects when I should be looking at the uniqueness of the relationship. Makes sense now, thanks.

[@therealmeisl5609]

3:03 (a^b)^c = a^(b*c) interpreted as a term of type algebra: you write down c -> (b -> a) ~ (b, c) -> a. This is not immediate. For uncurrying c -> b -> a gives (c, b) -> a, NOT (b, c) -> a. These are, in general, NOT the same function type! I see that a pair (c, b) can be trivially mapped into a pair (b, c). But how's the argument going here, exactly?

[@BartoszMilewski]

Notice that we are really talking about isomorphisms, not equalities. To go between a->b->c and (a, b)->c you need an isomorphism which is the pair of functions curry/uncurry. So adding just one more isomorphism between (a,b) and (b,a) (which is called "swap") is no big deal. This is all "up to an isomorphism."

[@therealmeisl5609]

I see. Thank you. But now I'm a bit puzzled: the (simpler) exponential object a^b really is the same as the function type object b->a, not just isomorphic, right? Oh, and btw: *Thank you such much for this magnificent lecture series!*

[@BartoszMilewski]

The notation (a->b) is mostly used for the exponential object in the category Hask of Haskell types and functions. The exponential object may be defined in other categories as well.

[@therealmeisl5609]

Ok, thx again. If I had gotten *that* wrong I would have been really puzzled...

[@RepublikSivizien]

0^a = undefined: a→void, so a function, that takes an a and never returns is undefined?

[@vladthemagnificent9052]

yes. literally undefined. you give it an element and there is not a defined value for it to correspond to in the void type. Imagine functions as look up tables. if the right column is empty for some given value, then we say that the function is undefined there.

[@MithicSpirit]

It is defined. In regular algebra, 0^a = 0 (for nonzero a), which can be translated to a -> Void ~ Void. This makes sense since the hom-set C(a, Void) is empty, which is equal to Void itself!

[@kingyinyan254]

My research is on applying logic to deep learning, to solve the problem of AGI. One amazing thing I discovered is that Google's BERT model can be viewed as a kind of alternative "logic" via the Curry-Howard correspondence. This insight points to ways to enhance BERT. I'm looking for partners to work on this :)

[@brandonbarker5448]

Regarding linear logic and linear types, ATS has linear types: www.ats-lang.org and targets C (and a lot of other interesting features): kzbin.info/www/bejne/sKWTgISYZql1odE

[@kahnfatman]

Sir, may I have a piece of your mind! I mean, you are a load of geek-puns.

[@enricomariadeangelis2130]

Is Either really the equivalent of OR? Or maybe Either is the equivalent of XOR??? See this: stackoverflow.com/a/64387100/5825294

[@MithicSpirit]

nothing there suggests that Either is the equivalent of xor, so I'm not sure where you got that from. Also, you can easily find that Either cannot be xor by comparing Either () () with true xor true. Either () () = {Left (), Right ()} is inhabited, while true xor true = false is uninhabited.

[@MagicGonads]

there is a decent point to be made about this because remember that the co-product was said to be the 'tagged' union, but there are other unions (namely the 'disjoint' union), in the 'disjoint' union all of the parameters must have an empty intersection, so this indeed corresponds to XOR. Up to isomorphism the 'tagged' union and the 'disjoint' union are the same, but that's the thing, we have concrete types in any given actual type system you actually use, so the distinction does matter. Up to isomorphism () = () but those two singleton sets can contain a different value.