Write a Blog >>
ICFP 2016
Sun 18 - Sat 24 September 2016 Nara, Japan
Sat 24 Sep 2016 11:45 - 12:10 at Conference Room 1 - Types and Effects

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).

Sat 24 Sep

hiw-2016-papers
11:45 - 12:35: HIW - Types and Effects at Conference Room 1
hiw-2016-papers11:45 - 12:10
Talk
Richard A. EisenbergBryn Mawr College
hiw-2016-papers12:10 - 12:35
Talk
Ben LippmeierUniversity of New South Wales