Explore the impact of dependent type theory on Haskell in this 39-minute Strange Loop Conference talk by Professor Stephanie Weirich. Delve into the adoption of dependent type-inspired features in the Glasgow Haskell Compiler (GHC) over the past decade. Examine an extended example to understand programming with dependent types in Haskell, and discover what works, what challenges remain, and unexpected insights gained from this language design experiment. Learn about compile-time parsing, type functions, GADTs, indexed types, singletons, and type classes in the context of dependent typing. Gain insights from Weirich's extensive experience in functional programming, type systems, and theorem proving, as she shares her expertise on the four key capabilities of dependent type systems and their practical applications in Haskell development.
Overview
Syllabus
Intro
Dependent Haskell
Regular expression capture groups
How does this work? 1. Compile-time parsing
2. Type functions run by type checker
Types Constrain Data with GADTS
Indexed Types constrain data
Dependent types
GHC's take: Singletons
Working with type indices
Type classes to the rescue
Four Capabilities of Dependent Type Systems
Taught by
Strange Loop Conference
