Developing Theories of Types and Computability via Realizability