Typing Extensible Data Types and Functions using Rows

Cas van der Rest

Date: Wed, November 17, 2021
Time: 12:00
Room: Cas' Zoom Room

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. |
Next: Aron Zwaan |