[marquis-chacha]

I think the idea is that it abstracts away a bunch of the area-specific stuff from other fields, distilling it all down to generalized reusable concepts. For instance, I watched the first lecture and saw immediate connections to the compatibility matrices used in programming language analysis and type theory. I didn't "learn" anything new from the lecture (it was all introductory), but I'm sure that if I keep up with the future lectures I'll see more that I can actually apply to my work.

[marquis-chacha]

Example: the first question on the first problem set [1] shows how the idea of the Least Common Multiple and the Greatest Common Divisor are analogous to ⊤ and ⊥ in PLT, or "any" and "never" in TypeScript. (Specifically, the Join and Meet operations)

[1]: https://ocw.mit.edu/courses/mathematics/18-s097-applied-cate...

[hopler]

LCM and GCD are meet and join (union supertype and intersection subtype in PLT), not top and bottom. Top/any would correspond to the product of all numbers (union of all factors), and bottom/never would correspond to 1 (intersection of all factors).

[smadge]

I don’t know PLT very well but wouldn’t top/bottom also be considered terminal/initial objects in categorical terms?

[auggierose]

For that you just need Lattice theory ...

[marquis-chacha]

Oh right, "Lattice" is the word I was looking for. It's been too long. Would that be considered a subset of category theory, a precursor to it, or another field that it somewhat "unifies"?

[smadge]

Lattice theory is it’s own field that exists outside of and before category theory. All lattices form a category, though, but not vice versa.