u/runT1MEin r/compsci • Recommends
Truth about Types (Lambda Days 2016): explains Curry-Howard-Lambek
0:00 / 0:00
#haskell#curry-howardisomorphism#typetheory
Bartosz Milewski - Truth about Types (Lambda Days 2016)
Erlang Solutions
18K subscribers • 48 videos on Hallway
- Recommended by 1 person: 1 in engineering communities.
- Presented by Bartosz Milewski
Advanced. Deep dive for people who know the field.
20K views10 years ago1 recommendation
Programming languagesComputer scienceLanguage design and type systemsComputation and complexityFunctional programming
Bartosz Milewski explains the Curry-Howard-Lambek isomorphism and how types encode logic in functional programming languages like Haskell.
Slides and more info: lambdadays.org/lambdadays2016/bartosz-milewski Lots of programmers, especially our brethren who use JavaScript, Python, or Closure, don't appreciate the power of strong static typing. Haskell programmers, on the other hand, eat types for breakfast, lunch, and dinner. Types are not just hints for the compiler to better catch programming errors. They encode logic. I'll talk about the Curry-Howard-Lambek isomorphism between types and logic. We can encode, in types, truth and falsehood; conjunction, disjunction, and implication; and let the Haskell compiler prove logical theorems for us.Why it's here
1 person recommends thisWhat people say. Recommended as an accessible introduction to the Curry-Howard isomorphism and type theory.