Variables in Types

September 25, 2017

These are some recitation notes for an ad-hoc recitation I gave for the class 15-312 Principles of Programming Languages. It was probably my favorite 312 recitation content-wise, because it’s the first recitation where we’ve covered enough stuff to where we can really start connecting the dots.


We’ve seen a number of examples in class of types which use variables. Having variables in our type systems lends a great deal of power to languages using these type systems. We’re going to look at how variables are used in generic programming, inductive & coinductive types, and polymorphic types.

Variables in Types

System Fω and Parameterization

Some recitation-style notes on System F, polymorphism, and functions. I used to not know the difference between ∀(t.τ) and λ(u.c). Turns out, there’s a huge difference! Continue reading

Recitation Notes

Published on September 24, 2017

Testing, Types, & Correctness

Published on September 10, 2017