Hype for Types is a student-run course at CMU teaching topics in type theory and related disciplines. It is aimed at students with only basic knowledge of functional programming, and designed to give them a high-level introduction to a variety of fascinating topics which could otherwise only be learned after years of detailed study. Some topics that have been covered in Hype for Types include: typechecking, lambda calculus, the Curry-Howard isomorphism, constructive logic, dependent type theory, category theory, Homotopy Type Theory, pure type systems, higher-order abstract syntax, phantom typing, (generalized) algebraic datatypes, subtyping, algebraic effects, Hoare logic, parsing, and compilation.
It is taught by Aditi Gupta, Avery Cowan, Harrison Grodin, and Matthew McQuaid.
Subject to change. After each lecture, the relevant notes/slides will be posted.
| Date | Topics | Notes | |
|---|---|---|---|
| 1 Sep | Simply-Typed Lambda Calculus | Slides | |
| 8 Sep | Algebraic Data Types | Slides | |
| 15 Sep | Constructive Logic & The Curry-Howard Isomorphism | Slides | |
| 22 Sep | Phantom Types and GADTs | Slides Code | |
| 29 Sep | Polymorphism and Unification | Slides | |
| 6 Oct | Category Theory (for Programmers) | Slides | |
| 13 Oct | Parsing with Monads | ||
| 20 Oct | Recursion Schemes | Live Code | |
| 27 Oct | Continuations & Classical Logic | Slides | |
| 3 Nov | Compilation | ||
| 10 Nov | Linear Logic, Rust, and Session Types | Slides Code | |
| 17 Nov | Dependent Types I | Slides | |
| 24 Nov | Cancelled for Thanksgiving | ||
| 1 Dec | Dependent Types II | Code | |
| 8 Dec | The Unknown? |
In general, it is expected that you attend every lecture synchronously. Lectures are designed to be interactive and fun, so whenever possible, please come hyped!
If you can't regularly attend synchronously (e.g. due to timezone), please let the instructors know. If you can't make it to a particular lecture, please let the instructors know ahead of time.
Every lecture will have a corresponding homework assignment to reinforce the content of the lecture and to give you additional practice with the topics covered. The homeworks are designed to follow readily from the lectures, and should not require a great amount of time or effort. In general, you shouldn't need to spend more than an hour on any given homework assignment.
Homeworks are mandatory, but they are graded for effort, not correctness. This means that you must attempt to correctly complete every homework, but if you put in a good faith effort and do not manage to finish it correctly, you will still recieve credit.
We understand that you're busy and might not have time to complete the homework the week it's assigned. That's okay! If you're not able to complete an assignment within one week (i.e. by the next lecture), please email us (or send us a direct message on Slack) to get an extension. However, please stay on top of the homeworks! We reserve the right to deny you an extension if you have too many homeworks outstanding.
Discussion of homework questions is always permitted in any form, including via Slack. However, direct copying of answers, whether code or written, is not permitted.