Havl7ifrvpamkxjnuud8
SkillsCast

Keynote: The Maths Behind Types

14th December 2017 in London at Business Design Centre

There are 53 other SkillsCasts available from Scala eXchange 2017

Please log in to watch this conference skillscast.

680599783 640

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:

Thanks to our sponsors

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.

SkillsCast

Please log in to watch this conference skillscast.

680599783 640

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:

Thanks to our sponsors

About the Speaker

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.

Photos