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 |
|---|---|---|
| Feb 2 | Simply-Typed Lambda Calculus | Slides |
| Feb 9 | Algebraic Data Types | Slides |
| Feb 16 | Constructive Logic & The Curry-Howard Isomorphism | Slides |
| Feb 23 | No Lecture: Break Day | |
| Mar 2 | Phantom Types and GADTs | Slides Code |
| Mar 9 | Linear Logic | Slides Code |
| Mar 16 | Recursion | Code |
| Mar 23 | Continuations & Classical Logic | Slides Code |
| Mar 30 | Compilation | Slides |
| Apr 6 | Polymorphism | Slides |
| Apr 13 | Category Theory (for Programmers) | Slides |
| Apr 20 | Dependent Types I | Slides |
| Apr 27 | Dependent Types II | Code |
| May 4 | The Unknown? | Jacob Cam Charles |
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.
If you have a disability and have an accommodations letter from the Disability Resources office, I encourage you to discuss your accommodations and needs with me as early in the semester as possible. I will work with you to ensure that accommodations are provided as appropriate. If you suspect that you may have a disability and would benefit from accommodations but are not yet registered with the Office of Disability Resources, I encourage you to contact them at access@andrew.cmu.edu