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:
- Lightbend Akka for Scala - Professional (in London on 11th - 12th November 2019)
- Modern development with Java (in London on 9th - 11th December 2019)
- Scala eXchange London 2019 (in London on 12th - 13th December 2019)
- Scalax2gether Community Day 2019 (in London on 14th December 2019)
- Solandra Hands-On Tutorial & Emergent Behaviour In Insects (in London on 28th October 2019)
- Don’t keep it to yourself - openness and honesty in the workplace (in London on 30th 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.