Data Juggling - Part 5 - Curry-Howard-Lambek Correspondence

An overview of the isomorphism between mathematical proofs, computer programs, and category theory.

This video is an overview of the famous isomorphism between mathematical proofs, computer programs and category theory. Constraints Liberate, Liberties Constrain — Runar Bjarnason youtube.com/watch?v=GqmsQeSzMdw Three Paradigms by Robert C. Martin (Uncle Bob) blog.cleancoder.com/uncle-bob/2012/12/19/Three-Paradigms.htm… Programming with Categories: youtube.com/playlist?list=PLhgq-BqyZ7i7MTGhUROZy3BOICnVixETS Category Theory by Bartosz Milewski (this was the #4 that I accidentally skipped towards the end of the video) youtube.com/watch?v=I8LbkfSSR58&list=PLbgaMIhjbmEnaH_LTkxLI7… This video is part of the following playlist: youtube.com/playlist?list=PLJGDHERh23x9Wzcbc7j9ZDl03tKQF5QDN Table of Contents 00:00:00 Introduction 00:02:14 Definition 00:05:42 Types as sets of values 00:12:34 Sum Types 00:29:12 Products 00:33:46 Algebraic Data Types (ADTs) 00:36:45 Exponentials 00:41:23 Equational reasoning 00:51:37 Parametric reasoning (Theorems for free) 00:58:18 Practical example 01:09:07 Summary Website: devinsideyou.com Patreon: patreon.devinsideyou.com Discord: discord.devinsideyou.com Telegram: telegram.devinsideyou.com Twitter: twitter.devinsideyou.com GitHub: github.devinsideyou.com LBRY: lbry.devinsideyou.com Install scripts: install.devinsideyou.com Giter8 templates: g8.devinsideyou.com Spotify concentration playlist: code.radio.devinsideyou.com Cheers and Happy Coding! #Scala #tutorial