CSU Applied Category Theory Seminar

This seminar will run in Fall 2024 weekly on Thursdays 3-4pm, location TBD. Below are the seminar organizers.

• James Wilson (Colorado State University)
• Wolfgang Bangerth (Colorado State University)

Youtube Channel

About

Wondering what this means? Modern applications have to cope with numerous, interrelated systems. Today, categories are being used to organize systems and insert theory where it is otherwise hard to find. Examples include data structures for cloud computing, data analysis, formal verification, causality, and more.

All levels of experience are welcome. We are a friendly group happy to answer questions and just as happy to learn something from you.

Current Topics

We will be reading through Philip Wadler’s “Theorems for free!”.

During the first half of the semester, we read the first three chapters of Brendan Fong and David Spivak’s “An Invitation to Applied Category Theory”.

We will also lightly use Bartosz Milewski’s “Category Theory for Programmers” as a secondary resource. This is available freely from the authors website.

Past Topics

See Past Talks for more details.

• Functional programming languages that also serve as proof assistants. Examples include Lean, Agda, and Idris.
• Topos and subobject classifiers.
• Program design as Math: introduction to types, categories for functional programming, the algebra of an API.
• Dependent and Homotopy Type Theory
• Theorems for Free.
• Folds & Flats in Apache’s Spark.
• Kleisli Composition and Categories.
• Monads and Adjunctions with examples.
• The Option Monad and Strict and Lazy Evaluation
• Algebraic Data Types and Pattern Matching Where are the categories in Haskell & Scala?
• Loops & Recursion: comparing compiled code in C, Java, and Scala.

We read extensively from

Functional Programming in Scala by Paul Chiusano and Runar Bjarnason

This thin book features some of the most surprising applications that will reshape how you think of applied mathematics. From the use of mundane axioms in abstract algebra to prove programs are bug free to application of complex constructions in category theory to remove side-effects and make code that works in smoothly in parallel. When you finish be sure to look also at the companion solution manual packed with many more gems.

As a perk, this book is inexpensive and comes with a digital copy as well so you can have it as quick guide wherever you go.

What programming language to learn?

You do not have to program a thing…but even the best theoretical physicist wants to play with a laser sometimes, and as mathematician should likewise want to play with a computer.

C/C++, Java, and Python are safe comfortable choices with lots of tutorials, but to discover the mathematics of programming you might prefer to pick up modern language such as Scala, Haskell, Swift, C#, or OCaml. Maybe even a proof assistant like Agda or Coq, or something in between like Idris and Lean.

It wouldn’t hurt either to start using Git or its social-media platform GitHub. Similar to LaTeX, it is a pain at first, but you learn Git so you can be more productive in the long run.

Some History

This seminar began as an excuse to let two professors brush up on things on the state of programming that had changed since they had spent their time in the trenches. To save on embarrassement it would be done in secret. And as to not waste the opportunity the students of the professors would be dragged along as well. They focussed on a functional language called Scala because it had the right balance of use and good deal of math in the mix. Since it was in private they would meet in the stairwell – the Scalawell.

Scalawell quickly became the worst-kept secret. New students and postdocs showed each week. We met to learn theory and applications of modern mathematics to modern programming. You didn’t have to program to participate, just come with a curiosity to puzzle about hard problems disguised as easy questions. Some even wrote a paper. Since the meetings were in “secret”, no question was too embarrassing to ask.

That is the ethos of the seminar today. Came, ask, and make abstraction useful to your goals.

CSU Applied Category Theory 2023 (get source code). Last build date: 2024-10-24.