Live data from Hacker News

Programming with Categories

brendanfong.com

11–20 of 113 posts

Re: Programming with Categories

#11
post #9

David Spivak and other folks at Azimuth Forum[0] have been great at providing high quality discussions on ideas in this course and others. Many thanks. [0] https://forum.azimuthproject.org

Good point and strongly agree. John Baez [0] also merits mention as the originator of Azimuth and the creator of the Applied Category Theory course [1] on the back of Fong & Spivak's paper [2].

[0]https://www.azimuthproject.org/azimuth/show/John+Baez [1]https://forum.azimuthproject.org/discussion/1717/welcome-to-... [2]http://math.mit.edu/~dspivak/teaching/sp18/7Sketches.pdf

Re: Programming with Categories

#12

As someone who respects functional programming (because it removes geniuses from competing in my space) here's a nice video https://www.youtube.com/watch?v=ADqLBc1vFwI What is the beautiful monospace font in the pdf here http://brendanfong.com/programmingcats_files/cats4progs-DRAF... ?

> What is the beautiful monospace font in the pdf t1xtt, from the txfonts package, freely available

Thank you! No ttf/otf though :)

Re: Programming with Categories

#13

As someone who respects functional programming (because it removes geniuses from competing in my space) here's a nice video https://www.youtube.com/watch?v=ADqLBc1vFwI What is the beautiful monospace font in the pdf here http://brendanfong.com/programmingcats_files/cats4progs-DRAF... ?

Oh, another Haskell can't do IO joke.

Re: Programming with Categories

#14
post #3

"We will assume no background knowledge on behalf of the student, starting from scratch on both the programming and mathematics." This is a fantastic "side effect" of the fact that category theory isn't built on any other mathematical knowledge. You don't even need even any arithmetics for that.

At a meta level, Category Theory requires some comfort with abstraction, which really only comes with a mathematical education. So while it may stand apart from much math, it relies on your strong mathematical foundations.

Re: Programming with Categories

#15
For those who might not realize: IAP is the period between semesters at MIT, roughly most of January. So this is is a quick, accessible introduction, not a heavy semester-long slog.

Re: Programming with Categories

#16

As someone who respects functional programming (because it removes geniuses from competing in my space) here's a nice video https://www.youtube.com/watch?v=ADqLBc1vFwI What is the beautiful monospace font in the pdf here http://brendanfong.com/programmingcats_files/cats4progs-DRAF... ?

[deleted]

Re: Programming with Categories

#17

As someone who respects functional programming (because it removes geniuses from competing in my space) here's a nice video https://www.youtube.com/watch?v=ADqLBc1vFwI What is the beautiful monospace font in the pdf here http://brendanfong.com/programmingcats_files/cats4progs-DRAF... ?

Oh, another Haskell can't do IO joke.

Yes, but this time it was a funny one. I laughed, and not just at AbstractSingletonProxyFactoryBean.

Gotta be able to laugh at yourself sometimes.

Re: Programming with Categories

#19
I've read a lot about Category Theory, and I'm amazed at the abstraction level that lets you compose with different mathematical domains (geometry, topology, arithmetic, sets, ...).

And yet, the current mathematics relies heavily on the ZFC set theory. Why is that ? (Is that assumption even correct ?)

From what I've learned so far, the set theory suffers from Russel's Paradox[0] (does the set of all sets that does not contain itself, contains itself ?). That's what motivated the formalization of Type Theory and the invention of Type Systems in programming languages.

According to wikipedia[1], some type theories can serve as an alternative to set theory as a foundation of mathematics.

It seems to me that the Category Theory fits the description. So why don't we see a huge "adoption" in math fields ?

Thank you in advance for your clarifications :)

[0] - https://en.wikipedia.org/wiki/Russell%27s_paradox [1] - https://en.wikipedia.org/wiki/Type_theory

Re: Programming with Categories

#20
post #19

I've read a lot about Category Theory, and I'm amazed at the abstraction level that lets you compose with different mathematical domains (geometry, topology, arithmetic, sets, ...). And yet, the current mathematics relies heavily on the ZFC set theory. Why is that ? (Is that assumption even correct ?) From what I've learned so far, the set theory suffers from Russel's Paradox[0] (does the set of all sets that does no…

> From what I've learned so far, the set theory suffers from Russel's Paradox

So-called "naive set theory" does, but my understanding is that this paradox (and others like it) sparked a crisis in mathematics that led to the creation of ZFC and others. ZFC is not known to be inconsistent (due to deep and technical reasons, I can't claim positively that it is consistent), and it was designed to avoid the paradoxes that plagued naive set theory.

Russell's type theory was another early contender for a formalism. For whatever reason (I'm not aware of all the details), Zermelo-Fraenkel set theory (later extended with the Axiom of Choice) won the popular mindshare. Personally, I'm more a fan of the Elementary Theory of the Category of Sets (ETCS) [1], which is indeed drawn from category theory. But it's equivalent in deductive power to ZFC, so what you pick mostly only matters if you're doing reverse mathematics. (This is what really answers your question, I think.)

Russell's type theory and modern type theories are distinct (and there is no single "type theory"). I'm led to believe the commonality is primarily with the usage of a hierarchy of universes, so that entities in one unverse can only refer to entities in a lower universe.

[1] "Rethinking set theory", Tom Leinster: https://arxiv.org/abs/1212.6543

Post reply on HN