Typing Extensible Data Types and Functions using Rows

Cas van der Rest

In ongoing work, we have been developing a meta language (working title Strachey) for defining and composing programming language components. One of the key challenges of designing a type system for this language is to retain static type safety of pattern matching definitions in light of future extensions of data types with new constructors. In this talk, I discuss recent experiments on developing a calculus with row types in which we can encode (and type) extensible functions over extensible data types. Eventually, the goal is to use this calculus as a core language for Strachey, providing a well-understood and principled foundation for the surface language. I will also discuss some of the remaining challenges, such as encoding row-typed effects, and providing decent error reporting when type checking Strachey by going through a core language.

---

Previous: t.b.a. | No seminar (SPLASH conference)
Next: Aron Zwaan | Deriving Incrementality-Related Program Properties from Scope-Graph-Based Type-Checkers