Computational Math Colloquium | Bartosz Milewski, Programming with Universal Constructions

MC 5501 and Zoom (email compmath@uwaterloo.ca for Zoom link)

Speaker

Bartosz Milewski | Programming Cafe

Title

Programming with Universal Constructions

Abstract

There isn’t that much difference between category theory or type theory and programming, especially since mathematicians started using computers to formalize their language. I will show how algebraic data types are defined and used in category theory, and how universal constructions can be translated from the visual language of arrows and diagrams to actual Haskell code. I will also talk about adjunctions and recursive data types.