A Taste of Type Theory • Bartosz Milewski • YOW! 2019

This presentation was recorded at YOW! 2019. #GOTOcon #YOW
yowcon.com
Bartosz Milewski - Founder of Reliable Software
ABSTRACT
We use types in programming, often without realizing how deeply rooted they are in the foundations of mathematics. There is a constant flow of ideas from type theory to programming (and back). We are familiar with algebraic data types; inductive types, like lists or trees; we've heard of dependent types and, in the future, we might encounter identity types and possibly get familiar with elements of homotopy type theory.
I can't possibly talk about all of this, but I'll try to give you a little taste. [...]
TIMECODES
0:00 Introduction
2:19 Outline
5:09 Equalities
9:51 Natural Numbers
16:29 Dependent Types
23:38 Induction on Nats
27:23 Curry Howard
30:28 Identity Type
35:36 refl
42:48 Elimination
52:51 Zeno's Paradox
/ gotocon
/ goto-
/ gotoconferences
#TypeTheory #Haskell #Programming #DataTypes #Algebra #BartoszMilewski #YOWcon
Looking for a unique learning experience?
Attend the next GOTO conference near you! Get your ticket at gotopia.tech
Sign up for updates and specials at gotopia.tech/newsletter
SUBSCRIBE TO OUR CHANNEL - new videos posted almost daily.
ua-cam.com/users/GotoConf...

[@markhathaway9456]

Brilliant stuff and ending with a bit of humor. I loved that he was hinting about all these theories (Set, Category, etc.) becoming so well understood that they are leading to one unified theory.

[@blacknick3931]

HoTT

[@jbragg33]

wut

[@jasenq6986]

type theory, dude

[@bigstones84]

@@jasenq6986 looks like I'm not the only one saving this video for Christmas...

[@jasenq6986]

@@bigstones84 based

[@jasenq6986]

I love dependent types and static checks