Slides and more info: http://www.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.