1. Types Are Theorems; Programs Are Proofs
2. Haskell function types
3. Currying
5. Which types are inhabited?
6. We know that _b_→_b_ is inhabited (id for example)
7. * _b_ → _a_ _is not_ inhabited
8. Intuitively, the answer is no.
9. Types can be understood as propositions
10. Examples of propositions
11. Propositions vs. types
12. How to decide if a proposition is true
13. Another proof
14. How to construct a function with any type
17. Big deal
18. Pairs
19. -??!- x :: a
20. Example
22. Examples with(out) proof
23. * “∨” means “or”
24. Union types
26. Example
28. Negation
30. Leftovers
32. Final remark
33. Thanks!