Principals of Programming Seminar

Thursday, December 5, 2019 - 3:30pm to 4:30pm


Traffic21 Classroom 6501 Gates Hillman Centers



Syntax and Semantics of Higher-Kinded Data Types

In this talk I will present a grammar for a robust class of data types — including ADTs, nested types, GADTs, and their higher-kinded analogues — and argue that all of the data types this grammar defines have endofunctor initial algebra semantics when the category C interpreting types is locally presentable. The key insight is that GADTs and their higher-kinded analogues are underspecified by their syntax, and that, in locally presentable categories, left Kan extensions can be used to propagate a data type's syntactic generators across the entire universe of types in such a way that its associated type constructor is completed to a proper endofunctor on C with a canonical action on morphisms. Since local presentability is needed to derive initial algebra semantics just of standard ADTs, our analysis shows that no additional categorical structure beyond that needed for ADTs is needed to support initial algebra semantics for the more advanced data types generated by our grammar. Our analysis also derives a precise measure of the semantic complexity of each data type generated by our grammar, given by the least cardinal lambda for which its underlying functor is lambda-accessible. When lambda is omega, this measure characterizes those data types whose data elements are effectively enumerable.

This talk reports on joint work with Andrew Polonsky.

Patricia Johann is a (Full) Professor in the Computer Science Department at Appalachian State University in Boone, NC, where she does research and teaches a variety of computer science courses. Before coming to Appalachian State University, she was a Reader (US equivalent: Professor) of Computer Science in the Mathematically Structured Programming group in the Department of Computer and Information Sciences at the University of Strathclyde in Glasgow, Scotland. While there she spent part of a sabbatical in 2012 at the Department of Computer Science and Engineering at Chalmers University in Gothenburg, Sweden.

Faculty Host: Steve Awodey

Event Website:

For More Information, Contact:


Seminar Series