Events Calendar

Speaker

J. Garrett Morris

Abstract

Functional programming languages assume that generic types—in the FP parlance, type constructors—are total. Yet functional programmers know better: counterexamples range from container types that make limiting assumptions about their contents (e.g., requiring computable equality or ordering functions) to type families with defining equations only over certain choices of arguments. This gap makes programs harder to write and more prone to error: more prone to error because invariants of data structures may be captured only informally; harder to write because partial type constructors may not benefit from abstractions over generic types.

We present a language design and formal theory of partial type constructors, capturing the domains of type constructors using qualified types. Our design is both simple and expressive: we support partial datatypes as first-class citizens (including as instances of parametric abstractions, such as the Haskell Functor and Monad classes), and show a simple type elaboration algorithm that avoids placing undue annotation burden on programmers. We have extended GHC, the most widely used Haskell compiler, with support for partial type constructors, and test our extension on the compiler itself and its libraries. We show that introducing partial type constructors has a minimal impact on most code, but raises important questions in language and library design.

Bio

J. Garrett Morris is an assistant professor in the Department of Computer Science at the University of Iowa. He received his Ph.D. from Portland State University in Oregon, and post-doctoral training at the University of Edinburgh, Scotland. His research focuses on the development of type systems for higher-order functional programming languages, with the twin aims of improving expressiveness and modularity in high-level programming and supporting safe concurrent, low-level, and effectful programming. His work has been published in the top venues in theoretical programming languages, and he has received an NSF CAREER award.