Generalized algebraic data types and all that

August 22, 2006
Martin Sulzmann | School of Computing of the National University of Singapore

Generalized algebraic data types (GADTs) extend algebraic data types by a form of type refinement connected to pattern matchings. There are numerous useful examples which exploit this feature such as type-safe evaluators etc.

In this talk, I take a closer look at the GADT type inference problem and investigate how to compile GADTs to a typed intermediate language. Specifically, I will explain why type inference for GADTs is such a hard problem and suggest possible solutions to guarantee complete and decidable type inference. I also argue for a combination of GADTs with other type extensions such as type classes. This provides the user with reasoning capabilities which used to be the domain of specialized tools such as logical frameworks and proof assistants.

Speaker Details

Martin Sulzmann is an Assistant Professor in the School of Computing of the National University of Singapore. Before joining NUS, he was a Lecturer in the Department of Computer Science and Software Engineering at the University of Melbourne (Australia). He obtained his PhD from Yale University (USA) in Computer Science. His undergraduate studies were undertaken at the University of Karlsruhe (Germany).His main research interests are the design, analysis and implementation of modern programming languages based on concepts such as type systems, constraints and logical environments. His research goal is to make software systems easier to write and maintain, more secure and more efficient to execute.More information can be found on his home-page: http://www.comp.nus.edu.sg/~sulzmann/