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, phantom typing, (generalized) algebraic datatypes, subtyping, lambda calculus, the Curry-Howard isomorphism, constructive logic, dependent type theory, category theory, Homotopy Type Theory, pure type systems, higher-order abstract syntax, algebraic effects, Hoare logic, parsing, and compilation.
It is taught by Thejaswi Kadur, Jacob Neumann, Cameron Wong, and Ariel Davis.
It was taught in the past by Vijay Ramamurthy, Jeanne VanBriesen, Chris Grossack, and Charles Yuan.
Subject to change. After the lecture, notes/slides will be posted under "What" and homework will be posted under "HW".
| When | Who | What | HW |
|---|---|---|---|
| 14 January | Jacob | Welcome, Intro to Type Theory | HW 01 |
| 21 January | Cam | Algebra, Calculus and Trees | HW 02 |
| 28 January | Avery | Curry-Howard Isomorphism (Guest Lecture) | HW 03 |
| 04 February | Thejas | Phantom Types & GADTs | HW 04 |
| 11 February | Cam | Subtyping | HW 05 |
| 18 February | Harrison | Type Inference (Guest Lecture) | |
| 25 February | Thejas | Substructural Type Systems/Rust | |
| 03 March | Matthew | Monadic Parser Combinators (Guest Lecture) | HW 08 (optional) |
| 17 March | CANCELLED | ||
| 24 March | Cam | Recursion Schemes | |
| 31 March | Jacob | Category Theory | |
| 07 April | Jacob | CPS & Category Theory | |
| 14 April | Thejas | Practical Dependent Types | |
| 16 April | Cam | Dependent Type Theory, Notes from F19 | HW 13 |
| 21 April | Jacob | Homotopy Type Theory I | |
| 28 April | Jacob | Homotopy Type Theory II |
We will be taking attendance at each lecture. StuCo policy states that if you miss more than two classes without prior notice, we cannot give you a passing grade for the class. So please let us know ahead-of-time if you cannot make it. Even if your absence is excused, you are still responsible for any homework assigned (see below). Please coordinate with that week's lecturer to get the content of the lecture, especially if lecture slides/notes are not posted.
For several of the lectures, we will be subsequently assigning homework 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. As a general rule, you shouldn't be spending much more than half-an-hour on each 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 post a private question to the instructors on Piazza) 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.
Please do not cheat.
Discussion of homework questions is always permitted in any form. However, direct copying of answers, whether code or written, is not permitted.