Value Your Types!

You’re probably familiar with types in programming languages, such as “integer” or “list of integers.” But what if your type system were powerful enough to express types like “non-negative integer” or “list of strings where each string is at least eight characters long”? Welcome to the world of dependent types! In this talk, we’ll explore what dependent types are, how they work, and the relationship between type theory and predicate logic, all using the Idris programming language. We’ll even see when type checking can become (gasp) undecidable! EVENT:
!!Con West 2019 SPEAKER:
Eric Weinstein PUBLICATION PERMISSIONS:
Original video was published with the Creative Commons Attribution license (reuse allowed) ATTRIBUTION CREDITS:
Original video source: https://www.youtube.com/watch?v=gioRL1VleBw https://www.youtube.com/watch?v=DYEHxkhylDI