Hype for Types is a student-run course (StuCo) at CMU teaching topics in type theory and related disciplines. It is designed to give students a high-level introduction to a variety of fascinating practical topics in type theory and programming language theory 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.
This course is aimed at students with a basic knowledge of functional programming, such as experience in Standard ML, OCaml, or Haskell. We will often use Standard ML in lectures and on homework assignments.
It is currently taught by:
Subject to change. After each lecture, the relevant notes/slides will be posted.
| Date | Topics | Notes |
|---|---|---|
| Jan 18 | Simply-Typed Lambda Calculus | Slides |
| Jan 25 | Algebraic Data Types and Type Arithmetic | Slides |
| Feb 1 | Constructive Logic & The Curry-Howard Isomorphism | Slides |
| Feb 8 | Phantom Types & GADTs | Slides, Code |
| Feb 15 | Linear Logic | Slides, Code |
| Feb 22 | OCaml Week: Row Polymorphism and Subtyping | |
| Mar 1 | Continuations & Classical Logic | Slides, Code |
| Mar 8 | No Lecture: Spring Break | |
| Mar 15 | Category Theory: Basics | |
| Mar 22 | Category Theory: Monads | |
| Mar 29 | Polymorphism | Slides |
| Apr 5 | Inference, Unification, and Hindley-Milner | |
| Apr 12 | Dependent Types I | Slides |
| Apr 19 | Dependent Types II | Code |
| Apr 26 | The Unknown? |
Students are expected to attend every class. Students that have more than 2 unexcused absences will automatically fail the course. This is a strict policy. Students with legitimate reasons to miss class should inform the instructors in advance as soon as possible. Lectures are designed to be interactive and fun, so whenever possible, please come hyped!
Attendance will be taken via a weekly poll.
We will use a private Discord Server for communication throughout the semester, including distribution of homework assignments. Additionally, we will use Gradescope for collecting and providing feedback on 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" (spend 30 to 60 minutes) and do not manage to finish it correctly, you will still receive 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 Discord) 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.
The instructors will provide prompt feedback on every homework submission via Gradescope. While it will include a "score", a non-zero score means that the homework was completed sufficiently. The "score" and feedback are purely to help you learn! Please feel free to reach out to the instructors to discuss the homeworks.
In order to pass the course, students must:
Discussion of and collaboration on homework questions is permitted and encouraged! However, direct copying of answers, whether code or written, is not permitted.
From CMU’s Policy on Academic Integrity: In any manner of presentation, it is the responsibility of each student to produce her/his own original academic work. Collaboration or assistance on academic work to be graded is not permitted unless explicitly authorized by the course instructor(s). Students may utilize the assistance provided by Academic Development, the Global Communication Center, and the Academic Resource Center (CMU-Q) unless specifically prohibited by the course instructor(s). Any other sources of collaboration or assistance must be specifically authorized by the course instructor(s).
In all academic work to be graded, the citation of all sources is required. When collaboration or assistance is permitted by the course instructor(s) or when a student utilizes the services provided by Academic Development, the Global Communication Center, and the Academic Resource Center (CMU-Q), the acknowledgement of any collaboration or assistance is likewise required. This citation and acknowledgement must be incorporated into the work submitted and not separately or at a later point in time. Failure to do so is dishonest and is subject to disciplinary action.
Instructors have a duty to communicate their expectations including those specific to collaboration, assistance, citation and acknowledgement within each course. Students likewise have a duty to ensure that they understand and abide by the standards that apply in any course or academic activity. In the absence of such understanding, it is the student’s responsibility to seek additional information and clarification.
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.
This semester is unlike any other. We are all under a lot of stress and uncertainty at this time. Attending Zoom classes all day can take its toll on our mental health. Make sure to move regularly, eat well, and reach out to your support system or Judy Hallinen [hallinen@cmu.edu] if you need to. We can all benefit from support in times of stress, and this semester is no exception. If you or anyone you know experiences any academic stress, difficult life events, or feelings like anxiety or depression, we strongly encourage you to seek support. Counseling and Psychological Services (CaPS) is here to help: call 412-268-2922 and visit their website at http://www.cmu.edu/counseling/. Consider reaching out to a friend, faculty or family member you trust for help getting connected to the support that can help.
We must treat every individual with respect. We are diverse in many ways, and this diversity is fundamental to building and maintaining an equitable and inclusive campus community. Diversity can refer to multiple ways that we identify ourselves, including but not limited to race, color, national origin, language, sex, disability, age, sexual orientation, gender identity, religion, creed, ancestry, belief, veteran status, or genetic information. Each of these diverse identities, along with many others not mentioned here, shape the perspectives our students, faculty, and staff bring to our campus. We, at CMU, will work to promote diversity, equity and inclusion not only because diversity fuels excellence and innovation, but because we want to pursue justice. We acknowledge our imperfections while we also fully commit to the work, inside and outside of our classrooms, of building and sustaining a campus community that increasingly embraces these core values. Each of us is responsible for creating a safer, more inclusive environment. Unfortunately, incidents of bias or discrimination do occur, whether intentional or unintentional. They contribute to creating an unwelcoming environment for individuals and groups at the university. Therefore, the university encourages anyone who experiences or observes unfair or hostile treatment on the basis of identity to speak out for justice and support, within the moment of the incident or after the incident has passed. Anyone can share these experiences using the following resources: