Chapter 5: Type Theory Design I: Realizability

Following a suggestion by a listener on the discussion forum, the fifth chapter of the Iowa Type Theory Commute is about basic considerations for designing a type theory. Actually, it is about just one such consideration: should types be erased from terms or should we consider that they persist at runtime? I come down strongly on the side of erasing types, and give arguments for why, as well as some further consequences for design of typed languages. Realizability is considered as relating to this point.