This course explores the influence of dependent types on the design of the Glasgow Haskell Compiler (GHC) and on the practice of Haskell programmers. By discussing an extended example, participants will learn what it means to program with dependent types in Haskell. The course covers topics such as compile-time parsing, type functions, GADTs, indexed types, singletons, working with type indices, and the capabilities of dependent type systems. The teaching method involves a lecture format with practical examples. This course is intended for individuals interested in functional programming, type systems, and language design, particularly those with a background in Haskell programming.
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
