Tomas Petricek

fsharpWorks

Tomas is a computer scientist and open-source developer. He is a Visiting Researcher at the Alan Turing Institute working on tools for open data-driven storytelling. He wrote a popular book called "Real-World Functional Programming" and is a lead developer of several F# open-source libraries. He is a partner at fsharpWorks where he provides trainings and consulting services. Tomas' PhD thesis at the University of Cambridge focused on context-aware programming, but his most recent writings also includes two essays try to understand programming through the perspective of philosophy of science.

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).

tomasp.net/academic/papers/against-types

Slides
Video ←Back

Contact

For general info: info@lambdadays.org
To become a sponsor: wioletta@lambdadays.org