LFCS Seminar: Friday 15 August: J Garrett Morris Title: On Extensibility Abstract:The expression problem is an old name for an older problem: to independently extend the definition of a data type and the operations over it, without recompiling existing code and while retaining static type safety. I am interested in an extension of the expression problem: to define data types and operations over them by combining independent definitions of smaller data types, and operations over those smaller types. As I will demonstrate, a solution to this problem provides both flexible combination of data types and functions and precise definitions of traversals over recursive data types.I will present the Rose type system, the current state of a line of work which (I claim!) solves the extended expression problem. Our work is founded on row types, which make structures of data first-class citizens of the type system. We have a novel approach to row typing, in which operations on rows are described by predicates in a qualified type system. Rose supports label-generic programming, an extension to row typing that captures generic programming patterns without relying on run-time type representation. We have extended Rose to recursive types, and discovered a new formulation of extensible recursive traversals. I will shown that the resulting system is sufficient to capture several examples of extensible programming, including extensible big-step and small-step evaluation relations, and modular definitions of desugaring and substitution.Rose has a formal model with the expected metatheory, mechanized in Agda, and an experimental implementation, sufficient to type check and evaluate the examples in the talk.Bio: J. Garrett Morris is an assistant professor and the inaugural Emeriti-Faculty Scholar 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, particularly on problems of extensibility and modularity. His work is supported by the National Science Foundation, including by a CAREER award. Aug 15 2025 11.10 - 12.00 LFCS Seminar: Friday 15 August: J Garrett Morris J. Garrett Morris The University of Iowa https://jgbm.github.io/ Note unusual day and time IF G.03
LFCS Seminar: Friday 15 August: J Garrett Morris Title: On Extensibility Abstract:The expression problem is an old name for an older problem: to independently extend the definition of a data type and the operations over it, without recompiling existing code and while retaining static type safety. I am interested in an extension of the expression problem: to define data types and operations over them by combining independent definitions of smaller data types, and operations over those smaller types. As I will demonstrate, a solution to this problem provides both flexible combination of data types and functions and precise definitions of traversals over recursive data types.I will present the Rose type system, the current state of a line of work which (I claim!) solves the extended expression problem. Our work is founded on row types, which make structures of data first-class citizens of the type system. We have a novel approach to row typing, in which operations on rows are described by predicates in a qualified type system. Rose supports label-generic programming, an extension to row typing that captures generic programming patterns without relying on run-time type representation. We have extended Rose to recursive types, and discovered a new formulation of extensible recursive traversals. I will shown that the resulting system is sufficient to capture several examples of extensible programming, including extensible big-step and small-step evaluation relations, and modular definitions of desugaring and substitution.Rose has a formal model with the expected metatheory, mechanized in Agda, and an experimental implementation, sufficient to type check and evaluate the examples in the talk.Bio: J. Garrett Morris is an assistant professor and the inaugural Emeriti-Faculty Scholar 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, particularly on problems of extensibility and modularity. His work is supported by the National Science Foundation, including by a CAREER award. Aug 15 2025 11.10 - 12.00 LFCS Seminar: Friday 15 August: J Garrett Morris J. Garrett Morris The University of Iowa https://jgbm.github.io/ Note unusual day and time IF G.03
Aug 15 2025 11.10 - 12.00 LFCS Seminar: Friday 15 August: J Garrett Morris J. Garrett Morris The University of Iowa https://jgbm.github.io/ Note unusual day and time
