Bartosz Milewski - Truth about Types (Lambda Days 2016)

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

[@bocckoka]

there should be a collectors edition of this on blueray with leather cover for the fans.

[@kahnfatman]

Next to the psychology of Jungs, Freud, Piaget -- there should be a school of psychology named after Prof Bartosz. He is absolutely crazy in a positive way.

[@DrakePitts]

At 37:57, the last line should read "unit _ = ()" to conform to proper Haskell syntax.

[@elcapitan6126]

What a great intro!

[@tdchayes]

1:01:46 is where the Intuitionistic Logic is brought forward.

[@scitwi9164]

01:06 Kinda reminds me the trick used in C (which didn't have the `bool` type) to use `int` values as booleans by double-negating them before use, like `!!x`, to make sure they're always `0` or `1` and not something else ;)

[@antonyanonym5578]

content starts at 12:50.

[@mortenbrodersen8664]

Much better at 1.75x speed