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.