98-317: Hype for Types


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.


Spring 2020 Schedule

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)
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.

Academic Integrity

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.