27 ms·
Programming with Categories
- iso8859-1 6y agoVideos of the lectures from last year: https://www.youtube.com/watch?v=NUBEB9QlNCM https://www.youtube.com/watch?v=NUBEB9QlNCM
- nwallin 6y agoHere's the full playlist: https://www.youtube.com/playlist?list=PLhgq-BqyZ7i7MTGhUROZy3BOICnVixETS https://www.youtube.com/playlist?list=PLhgq-BqyZ7i7MTGhUROZy...
- mcalus3 6y ago"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.
- qppo 6y agoto get super meta, one could say that the opposite is true: arithmetic requires categories
- dan-robertson 6y agoExcept 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)
- housecarpenter 6y agoYou should read the famous book by Linderholm, Mathematics Made Difficult
- spirographer 6y agoAt 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.
- dkarl 6y agoAs so many undergraduate math textbooks say, "No background is assumed beyond sufficient mathematical maturity."
- mcguire 6y ago"Sufficient mathematical maturity": https://c8.alamy.com/comp/HY1PD9/elderly-math-teacher-HY1PD9.jpg https://c8.alamy.com/comp/HY1PD9/elderly-math-teacher-HY1PD9...
- deleted 6y ago[deleted]
- pizza 6y agoWhich 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
- dan-robertson 6y agoPeople 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?)
- picklenerd 6y agoThis 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.
- Someone 6y agoIf 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 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.
- Tainnor 6y agoYeah, 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.
- hawkice 6y agoIn my experience, Monad, Applicable, and Monoid are probably the only ones I'd use in Haskell, and maybe none of them in languages without good inference and general support. Pretty wild ideas, though. Fair chance they'd be more confusing than using more specifically named instances, but solid ideas where the class instance documents that you're using the pattern, instead of describing the preferred interface.
- Ericson2314 6y agoThere is sort of a "jump" from those to the ones less oriented around (->) but truer to the math, but I can assured I have in fact used https://hackage.haskell.org/package/categories https://hackage.haskell.org/package/categories (a prime example of the latter sort) in production and it was genuinely useful.
- smabie 6y agoYou've definitely used Functors or Semigroups as well, you just didn't realize it.
- tsimionescu 6y agoHere is my problem with these ideas in programming: if you recognize that some common construct is in fact a semigroup or functor, does knowing this actually buy you anything? I suppose it might help sometimes when designing an abstraction, to guide you to some nice properties, such as easy composition.
- codygman 6y ago> if you recognize that some common construct is in fact a semigroup or functor, does knowing this actually buy you anything? At least in Haskell one thing it means is you can use lots of new helper functions. > guide you to some nice properties, such as easy composition. Yep, which gets you code re-use for one.
- rotifer 6y agoWhile playing around with a problem at work involving Markov chains and graph connectivity, I found it useful to know that I could write (in Java) a generic method that performed "exponentiation by squaring" on semigroups. So, in addition to being able to raise numbers to powers I could also use it on matrices whose elements belonged to a semiring. That is, I could use the same code on a matrix of doubles with "times" and "plus" (for the Markov chains), as well as a matrix of booleans with "and" and "or" (for the graph connectivity). (Of course, I could have used special purpose libraries, but these were small problems and it was fun. :)
- max68 6y agoThese guys wrote "An Invitation to Applied Category Theory." It's an awesome book, and I'm super excited for these lectures.
- yearoflinux 6y agoAs 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 https://www.youtube.com/watch?v=ADqLBc1vFwI What is the beautiful monospace font in the pdf here http://brendanfong.com/programmingcats_files/cats4progs-DRAFT.pdf http://brendanfong.com/programmingcats_files/cats4progs-DRAF...?
- enriquto 6y ago> What is the beautiful monospace font in the pdf t1xtt, from the txfonts package, freely available
- yearoflinux 6y agoThank you! No ttf/otf though :)
- vertebrate 6y agoIt looks like a fork of Luxi Mono with slashed zero, which is available in ttf. And there is a more modern version of it with better character coverage -- Go Mono.
- marcosdumay 6y agoOh, another Haskell can't do IO joke.
- mumblemumble 6y agoYes, but this time it was a funny one. I laughed, and not just at AbstractSingletonProxyFactoryBean. Gotta be able to laugh at yourself sometimes.
- marcosdumay 6y agoThanks 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.)
- apkallum 6y agoDavid 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 https://forum.azimuthproject.org
- spinningslate 6y agoGood 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 https://www.azimuthproject.org/azimuth/show/John+Baez [1]https://forum.azimuthproject.org/discussion/1717/welcome-to-the-applied-category-theory-course#latest https://forum.azimuthproject.org/discussion/1717/welcome-to-... [2]http://math.mit.edu/~dspivak/teaching/sp18/7Sketches.pdf http://math.mit.edu/~dspivak/teaching/sp18/7Sketches.pdf
- read_if_gay_ 6y agoIs this Spivak related to the author of the famous Calculus book?
- dan-robertson 6y agoDavid and Michael Spivak are not related
- gumby 6y agoFor 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.
- random3 6y agoWow, what a combo! I'd be interested in anything from each of the lecturers, but all 3 at the same course, is amazing. Category Theory could be the rosetta stone of many things(this is relevant https://arxiv.org/pdf/0903.0340.pdf https://arxiv.org/pdf/0903.0340.pdf).
- linkdd 6y agoI'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 https://en.wikipedia.org/wiki/Russell%27s_paradox [1] - https://en.wikipedia.org/wiki/Type_theory https://en.wikipedia.org/wiki/Type_theory
- Twisol 6y ago> 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 https://arxiv.org/abs/1212.6543
- 6y ago
- razster 6y agoWhat an odd coincidence that this was posted and on my YT subscribe page: https://www.youtube.com/watch?v=NUBEB9QlNCM https://www.youtube.com/watch?v=NUBEB9QlNCM - Just posting the video for others to see.
- mncharity 6y agoWhen taught in January at MIT, a highlight was something I'd not seen elsewhere: someone called it the "aftermath" (3-pun). After the one-hour traditional-ish lecture (on video), the room was reserved for an additional hour. When previously taught, people would remain afterwards to ask questions, discuss math, and chat. So this was an iterative-improvement formalization of that. People would gather in front of the blackboards in fluid discussion clusters. Catalyzed by the three instructors and wizzy others, not all having to stay for the entire hour, but drifting off as discussion died away. They could show material they had pruned from the lecture, for want of time. Or got dropped as they ran over. Alternate presentation approaches they had considered, before selecting another. They could be much more interactive. One commented roughly "If I was tutoring someone, I'd never present the material this way". It was a delightful mix of catching the speaker after a talk to ask questions, a professor's office hours, a math major's lounge, an after-talk social, tutoring, an active-learning inverted classroom, hanging out with neighbors in front of the hallway blackboard, chalk clattering and cellphones clicking to snag key insights... It was very very nifty. So, the book is nice. And lecture notes. And videos. But... the best part isn't there. Perhaps the next iterative improvement is to capture the aftermath on video, and share that too. And as we look ahead, planning distance-learning and XR tools... maybe something like this is a vision to aspire too. The insane ratio of expertise to people learning is not something one can plausibly replicate in meatspace. But as conversations in front a virtual blackboard gradually become technically feasible, something like this might pay for the cost of it, with transformative impact.
- mortdeus 6y agowait, you are saying that at MIT you had to sit for a video? Why are you paying for that nonsense?
- mortdeus 6y ago" not all having to stay for the entire hour," No F that. If everybody (or their benefactor) is paying literally paying $666 (no joke thats what 40,000/60 equates to) everytime they show up to class, then everybody and their mother who decides to open their mouth can stay for the full 60 mintutes to hear the same stupid questions asked and answered over and over again. Thats the minimalistic price of having socialism/marxism show up on my favorite programming language golang.org thank you very much.
- Myrmornis 6y agoWill the course be taught live again and if so will those geographically elsewhere be able to attend?
- LockAndLol 6y agoThis doesn't work at all with HTTPS Everywhere. Just get a page about DreamHost site not found.
- mortdeus 6y agothe second i saw haskell i started saying eternally, "ABORT ABORT!" You are going to have to revive jesus to come up with a functional language that simplifies coding over a procedural one. Especially over an object oriented one.
- sideeffffect 6y agoIf you're interested in how Category theory and Algebra can inform the design of software, have a look at ZIO Prelude. https://github.com/zio/zio-prelude https://github.com/zio/zio-prelude It's a brand new library for Scala that contains reusable mathematical structures. Still based on algebra and category theory, but it expresses them more or less differently than how they've been expressed in Haskell (and similar languages). For example, unlike Haskell (and Scala's own cats and ScalaZ), it doesn't present the "traditional" Functor -> Applicative -> Monad hierarchy. Instead, it presents the mathematical concepts in a more orthogonal and composable way. One example out of many, you don't have a Monad. You have two distinct structures: * Covariant functor, with typical map operation `map[A, B](f: A => B): F[A] => F[B]` * IdentityFlatten which has a flatten operation `flatten[A](ffa: F[F[A]]): F[A]` and an identity element `any: F[Any]` When combined together (Scala has intersection types), you get something equivalent to the traditional Monad. The project is in its infancy, so it may still change significantly, though. Look here for more detailed explanation: https://www.slideshare.net/jdegoes/refactoring-functional-type-classes https://www.slideshare.net/jdegoes/refactoring-functional-ty... https://www.youtube.com/watch?v=OwmHgL9F_9Q https://www.youtube.com/watch?v=OwmHgL9F_9Q
- tsss 6y agoAre there any useful types that have `flatten` but not `map` or `contraMap`?
- sideeffffect 6y agoIf I understood John's motivation from the video, it's that this enables the Flatten structure to be inspectable, because the innards are not hidden behind an opaque closure (A => F[B]), as is the case in regular Monad. Btw, this is a problem that the "Selective applicative functor" too aims to alleviate. You can read more about the inspectability problem (and Selective) at http://eed3si9n.com/selective-functor-in-sbt http://eed3si9n.com/selective-functor-in-sbt The context there is sbt, which is a build tool, but I'm sure the inspectability plays role in many other areas. Note, how he contrasts "Applicative composition" and "Monadic composition".
- SJC_Hacker 6y agoDoes it compile to WebAssembly VM? Any compilers on Android or iOS? Will it work with Docker? Is it deployable on AWS or Azure?
- deleted 6y ago[deleted]
- aeontech 6y agoFor a humorous use case of types, nothing has beat Aphyr's (of Jepsen fame) "Typing the Technical Interview" here: https://aphyr.com/posts/342-typing-the-technical-interview https://aphyr.com/posts/342-typing-the-technical-interview If you haven't read it, take a minute...