Datatype-generic programming and practical subtyping for dependently-typed languages

Lucas Escot


Date: Wed, January 12, 2022
Time: 11:00
Room: Lucas' Zoom Room
Note: This is a PhD Go/No-Go meeting


In languages like Haskell or Ocaml, where programmers are encouraged to introduced new datatypes at will to suit the problem at hand, some machinery is made available in the language itself to relieve users of the burden of reimplementing basic constructions again and again. With such a deriving mechanism, users can retrieve things like decidable equality for free. In Agda however, such a practical system is not available as is. Reflection is powerful and can get you quite far, but it’s complex, tedious, and uses an untyped representation of terms.

In this presentation, I will showcase what has been the the main focus of this first year of work: A library for typed datatype-generic programming in Agda. It allows implementors to define constructions for all datatypes in regular safe Agda, and library users to derive a collection of generic constructions for free, for any of the datatypes they introduce by hand.

Then, I will introduce and motivate what I have since started to work on: pratical subtyping for dependently-typed languages.

Previous: Leonhard Applis |
Next: Aron Zwaan |