Tomas Petricek

fsharpWorks

Tomas is an academic, open-source developer and a book author. He is a lecturer at University of Kent and works on making programming with data easier. He also studies history of programming and writes about it from a philosophical perspective. Previously, Tomas wrote a popular F# book "Real-World Functional Programming", helped to create a number of F# open-source libraries such as F# Data and created coeffects (http://tomasp.net/coeffects), a theory of context aware programming languages. His most recent work includes programming tools for data journalism (http://thegamma.net), but also three essays that understand programming concepts such as types, monads and errors from philosophical perspective (http://tomasp.net/academic).

History and philosophy of types

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