Please log in to watch this conference skillscast.

You often think of types as specifying data layouts in computer memory. You have bytes, shorts, floats, and arrays, which are very close to the metal. But then you have integers and Booleans, which are abstractions taken from math. And then there are algebraic data types, and function types. During this talk, you can discover where these come from. There is some fascinating math behind types that you can learn from. It was first developed to avoid paradoxes in the naive set theory, and then it was linked to constructive logic and category theory. For instance, did you know that function types are defined in a cartesian closed category (Bartosz will share what it is)? Or that implementing a function is equivalent to proving a theorem? This "higher math" is actually quite approachable, if you're a programmer.

**YOU MAY ALSO LIKE:**

### Keynote: The Maths Behind Types

##### Bartosz Milewski

Bartosz started as a physicist. He has a Ph.D. in quantum field theory. Then he got into programming, worked eight years for Microsoft as a software engineer implementing the search engine in Windows. He wrote a book about C++ and started a popular programming blog. He rediscovered his fascination with mathematics through Haskell. His blog turned into an online book on category theory for programmers.