This talk will include three examples, compilable today, of dependently typed programming in Haskell:

• A finely-typed database access library whereby the requirements placed on the schema of the database can be inferred from the client code. This means that the database and the access code can be updated independently of one another, as long as the schema meets the inferred requirements.

• A datatype design pattern allowing for both row and column extensibility. This example makes critical use of both an injective type family and a higher-rank kind.

• A translation of Idris’s algebraic effects library to Haskell, allowing for client code to use several effects (such as state, failure, or I/O) together in a composable fashion without monad transformers or manual lifting.

The goal of this talk is not to explain all of the details of any of these examples, nor is it to advertise any release-ready software expected to be used in your next project. Instead, this talk is intended to showcase the kinds of problems dependent types in Haskell might solve and a sneak peek at some solutions.

Assistant Professor at Bryn Mawr College. I completed my PhD in 2016 at University of Pennsylvania working under Stephanie Weirich; my dissertation topic was the integration of dependent types into the Haskell programming language. I am a regular contributor to the Glasgow Haskell Compiler (GHC).