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.

Spring 2021 Schedule

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

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.

Acommodations and Disability Services

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

Previous Instances