Dependent types are everywhere! by Elisabeth Stenholm

Elisabeth Stenholm explains what dependent types are and how they provide compile-time guarantees using practical examples.

Have you ever heard of dependent types? Even if you have not, chances are you have most likely encountered some data structure that is actually dependently typed, without knowing it. In this talk I will explain what dependent types are and why they are everywhere, we just don’t notice them as we are so used to living without them. With dependent types we can express our structures more correctly, giving us more guarantees compile time. As a concrete example I will share my recent experience with writing a small questionnaire with a web frontend, all the parts of this construction that are actually dependently typed, and the differences between writing it with and without dependent types. Elisabeth Stenholm Elisabeth is 32 years old, born in Uppsala and raised in Stockholm. She has a PhD in dependent type theory from the University of Bergen, and is currently working as a fullstack developer at Frende Forsikring — a Norwegian insurance company based in Bergen. In her workday, Elisabeth writes primarily in the functional languages F# and Elm. She is passionate about type theory and functional programming, and enjoys sharing her knowledge on these topics with others. LinkedIn: linkedin.com/in/elisabethstenholm/ Code: github.com/elisabethstenholm/questionnaire === Video sponsor – Ada Beat === adabeat.com === Merch === If you want to spread functional programming and support the channel, buy something from the shop: funcprogsweden.myspreadshop.net/ 00:00 Stream starts 00:20 Dependent types are everywhere! by Elisabeth Stenholm 00:50 Onde does not simply create a questionnaire 02:49 Dependent types 07:32 OOP, FP, FP with dependent types 08:26 Questionnaires are dependently typed! 13:45 Snippets in Idris2 27:59 Demo 29:50 Takeaway 35:54 Q & A #funcprogsweden