Tomas Petricek

Tomas is a computer scientist, finishing his PhD at the University of Cambridge. He has been using F# since the early Microsoft Research versions many years ago.

He is the author of the popular (and F#-centric) book Real World Functional Programming, and has written numerous articles and StackOverflow answers. He has been a Microsoft C# MVP since 2004. He is also a frequent speaker at F# and .NET events, and a founding member of the F# Foundation.

He is the creator of the FSharp.Formatting library and has made major contributions to libraries such as FSharp.Data and Deedle.


NewCrafts 2017

 

History and Philosophy of types

  • talk
  • Functional
  • Theory
  • Practices

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