Skip to main content
Upcoming Events:
Seminar: Stephanie Weirich, University of Pennsylvania

Seminar: Stephanie Weirich, University of Pennsylvania

Date & Time:
   Add All to Calendar
Location:

ITB 201

Event Contact:

Fei Chiang, Jacques Carette

Overview

DEPENDENT TYPES IN HASKELL

What has dependent type theory done for Haskell? Over the past ten years, the Glasgow Haskell compiler (GHC) has adopted many type system features inspired by dependent type theory. In this talk, I will discuss the influence of dependent types on the design of GHC and on the practice of Haskell programmers. In particular, I will walk through an extended example and use it to analyze what it means to program with with dependent types in Haskell. Throughout, I will will discuss what we have learned from this experiment in language design: what works now, what doesn't work yet, and what surprised us along the way.

Speaker Bio: Stephanie Weirich is a Professor of Computer and Information Science at the University of Pennsylvania. She has published broadly in the areas of functional programming, type systems, machine-assisted theorem proving and dependent types. During the past ten years, she and her students have made significant contributions to the design of the Glasgow Haskell Compiler and its type system. Dr. Weirich has served as the program chair of the  ICFP 2010 and the 2009 Haskell Symposium and is also an editor of the Journal of Functional Programming. Her recent awards include the 2016 Most Influential ICFP Paper award (for 2006) for the paper "Simple unification-based type inference for GADTs" and the 2016 ACM SIGPLAN Robin Milner Young Researcher Award.