Katarzyna Marek: Dependently-typed regex parsers. Idris2-TyRE and associated project

Abstract: Regexes are widely used not only for validating but also for parsing textual data. Generally, regex parsers output a very generic structure, e.g. an unstructured list of matches, leaving it up to the user to validate the output's properties and transform it into the desired structure. Since the regex itself carries information about the structure, this leads to unnecessary repetition.

In this talk, we present a library for type-driven regex parsing (Idris2-TyRE). The idea behind the TyRE library is based on Radanne’s typed regexes library of the same name - a typed, indexed combinators layer that can be added on top of an existing regex engine. In contrast to Radanne's design, we also implement a parser, which maintains type safety throughout all layers. The parser is implemented in Idris 2 utilising the following features of Idris 2's advanced type system. We take advantage of type-level computation to establish the correct parse tree type; we use dependent-type verification to ensure the result type correctness; and we benefit from quantitative types by erasing the proofs and avoiding run-time overhead.

In the talk, I will also cover two downstream projects. and two associated projects: a sound and complete regex parser (Parse View) that uses McBride and McKinna’s dependent views, and a type-driven stream editor based on GNU sed that takes advantage of Idris2-TyRE.

This is joint work with Ohad Kammar and James McKinna.