98-317: Hype for Types

About

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.

Links

Fall 2020 Schedule

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
3 Nov Compilation
10 Nov Linear Logic, Rust, and Session Types
17 Nov Dependent Types I
24 Nov Cancelled for Thanksgiving
1 Dec Dependent Types II
8 Dec The Unknown?

Policies

Attendance

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.

Homeworks

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.

Academic Integrity

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.

Previous Instances