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.
kzread.info...