The arithmetic of types

Jeremy Gibbons ( OUCL )

In October I gave a talk about abstract types, explaining the slogan that "abstract datatypes have existential type". Existential quantification over types is analogous to existential quantification in logic; indeed, this is just one part of a much wider parallel between types and logic, called the "Curry-Howard Isomorphism" or "propositions as types". In this talk, I'll tell another part of the story, looking at the parallel between types and arithmetic - particularly at the laws of exponentials, and at recursive type equations. This is more than just fun mathematics: I will explain why I think it is also relevant to questions about service interoperability and model-driven data migration, which have been discussed at previous seminars.