Live data from Hacker News

Programming with Categories

brendanfong.com

51–60 of 113 posts

Re: Programming with Categories

#51
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.

I think I got more appreciation of abstraction from physics and programming than what mathematical education I had; I'm weak at maths -- experimental physics doesn't need much :-/ -- but I do understand that weakness, and am quite comfortable with abstraction.

Re: Programming with Categories

#52
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

Is this Spivak related to the author of the famous Calculus book?

Re: Programming with Categories

#54

Earlier quoted context omitted.

Yes, but this time it was a funny one. I laughed, and not just at AbstractSingletonProxyFactoryBean. Gotta be able to laugh at yourself sometimes.

Thanks for replying. I gave up on the beginning because those jokes tend to always be the same. (And to be fair, half of them are the same overused ones. But the others are good.)

"Thank god you haven't found Prolog..."

Re: Programming with Categories

#55
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…

ZFC does not suffer from Russel’s paradox, since it doesn’t allow a “set of all sets”. If it did, the search for new foundations would be much more widespread. New foundations are usually only considered seriously once they can be shown to be relatively consistent with ZFC or the slightly stronger but still uncontreversial TG set theory. There are people working on categorical foundations, but the main reason for lac…

It is not true that "basically every field uses its concepts and notation to some degree at this point." In particular this is false for mainstream combinatorics, PDE, and probability theory, to give a few examples.

In fact, I would suggest that most mathematicians don't care about category theory at all.

Re: Programming with Categories

#56
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…

IANAM, but... 1. I thought mathematics was moving more towards a category theory based foundation, as opposed to the set theoretical stuff. 2. Isn't it in part because we have over 120 years of results and proofs that are based on set theory, and people aren't just going to throw that out for something newer? Granted, Category Theory has been around in some form since about the 1940's, but it's still newer than set t…

1. It's not. The work on "category-theoretic foundations," say HoTT, is (sociologically speaking) a highly niche topic. Most professional mathematicians who work on the foundations of mathematics do so in the framework of set theory.

2. ZFC is fully adequate for all the mathematics 99% of professional mathematicians do (and probably more than adequate in terms of strength). Also, all the mathematics 99% of mathematicians do is insensitive to foundational issues, so if you swapped ZFC for another axiomatization of similar strength, no one would notice.

3. I don't believe ZFC was the first to avoid the paradox, but yes, it does not suffer from Russell's Paradox.

Re: Programming with Categories

#57
post #45

Earlier quoted context omitted.

This is almost every upper division undergrad math class. It was always fun watching people squirm when they pulled out some useful fact from their past 14 years of math education and then got told they had to prove it before they could use it.

If only it were limited to facts learned from math education. For example, there’s the Jordan curve theorem ( https://en.wikipedia.org/wiki/Jordan_curve_theorem ), which I guess most four-year olds ‘know to be true’ from their experience with coloring books.

Yeah, but from that same Wikipedia article:

> It is easy to establish this result for polygons, but the problem came in generalizing it to all kinds of badly behaved curves, which include nowhere differentiable curves, such as the Koch snowflake and other fractal curves, or even a Jordan curve of positive area constructed by Osgood (1903).

So to some extent, the reason why such an "obvious" statement requires a complicated proof is because our everyday notions of what a "closed curve" is are much more restricted than what we consider in mathematics. This is kind of common in maths, especially in fields with a lot of visual intuition.

Re: Programming with Categories

#58

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.

I think the joke was that Haskell can do IO but haskellers can’t

Re: Programming with Categories

#59
post #39
post #27

Earlier quoted context omitted.

As so many undergraduate math textbooks say, "No background is assumed beyond sufficient mathematical maturity."

Which is kind of ironic, because students take classes exactly because they feel 'immature' with respect to that subject.. Honestly, most of my smoothest educational experiences with hard topics assumed some immaturity on my part, and that that was OK

People don’t generally take category theory because they don’t really understand how proofs work or how to read definitions. The maturity required is about being able to cope with proving things and following proofs based on definitions which will probably seem somewhat bizarre at first and unmotivated at first. The immaturity you seem to talk about is people taking category theory because they don’t know category theory but that’s different and not what is meant by mathematical maturity.

That said, a background in mathematics helps with category theory. Things like group theory, topology (particularly algebraic topology), Galois theory and set theory can be useful in motivating a lot of category theory. I’m yet to see much of a strong motivation from programming (where is there a functor that isn’t an endofunctor?)

Re: Programming with Categories

#60
post #7
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.

to get super meta, one could say that the opposite is true: arithmetic requires categories

Except this isn’t really true in the common sense meaning (schoolchildren do arithmetic fine without knowing about category theory) or in the formal sense you’re trying to get at (there are formal axiomatic foundations which arithmetic can be based on which do not need category theory. A simple proof is by causality: arithmetic was successfully formalised before category theory was invented)
Post reply on HN