Slides and more info: lambdadays.org/lambdadays2016/tomas-petricek
What are types? We can try to answer this question with a formal definition. But there are numerous incompatible definitions and they fail to capture important aspects of what types actually are - how are they used in practice, how we talk about them and how we think about them. Why we often cannot even find a common language when talking about types?To think about these questions, we need to step outside of the neat world of mathematics and seek the bigger picture through history and philosophy of science. I'll introduce the history of types and explore how different people in different times thought about types over the last 100 years. Then, I'm going to discuss a number of theories from philosophy of science that explain some of the interesting historical developments, incompatibilities and changes in meaning.
Expect a thought-provoking talk involving the most famous works on types in mathematics and computer science (including Bertrand Russell's ""Principia Mathematica"" and Alonzo Church's simple theory of types), but also amazing ideas from philosophy (like Imre Lakatos's theory of research programmes and Paul Feyerabend's epistemological anarchism).
Looking at philosophy of science also helps us understand why there are so many misunderstandings and why answering the question ""what are types?"" is difficult. It turns out that this is normal and even necessary thing in science. In fact, as historical evidence suggests, having a clear and precise formal definitions can ""hamper the growth of knowledge"" (Lakatos) and ""deflect the course of investigation into narrow channels of things already understood"" (Feyerabend).