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:
- Leonardo De Marchi's Deep Learning Fundamentals (in London on 22nd - 23rd October 2019)
- Lightbend Akka for Scala - Professional (in London on 11th - 12th November 2019)
- Scala eXchange London 2019 (in London on 12th - 13th December 2019)
- Scalax2gether Community Day 2019 (in London on 14th December 2019)
- Security in the Age of Big Data (Data Anonymisation & Encryption) (in London on 21st October 2019)
- Code Kata: Yilin Wei - Optics with Monocle (in London on 22nd October 2019)
- Higher-Order Type-Level Programming (SkillsCast recorded in October 2019)
- Stick to Simple Haskell (SkillsCast recorded in October 2019)
Keynote: The Maths Behind Types
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.