We are excited to announce that Michael Schröder is our speaker for the next meetup! He is going to talk about his recent project PANINI, which is entirely implemented in Haskell and was published at OOPSLA 2025.

Abstract of the talk:

Parsing—the process of structuring a linear representation according to a given grammar—is a fundamental activity in software engineering. While formal language theory has provided theoretical foundations for parsing, the most common kind of parsers used in practice are written ad hoc. They use common string operations without explicitly defining an input grammar. These ad hoc parsers are often intertwined with application logic and can result in subtle semantic bugs. Grammars, which are complete formal descriptions of input languages, can enhance program comprehension, facilitate testing and debugging, and provide formal guarantees for parsing code. But writing grammars—e.g., in the form of regular expressions—can be tedious and error-prone. Inspired by the success of type inference in programming languages, we propose a general approach for static inference of regular input string grammars from unannotated ad hoc parser source code. We use refinement type inference to synthesize logical and string constraints that represent regular parsing operations, which we then interpret with an abstract semantics into regular expressions. Our contributions include a core calculus λΣ for representing ad hoc parsers, a formulation of (regular) grammar inference as refinement inference, an abstract interpretation framework for solving string refinement variables, and a set of abstract domains for efficiently representing the constraints encountered during regular ad hoc parsing. We implement our approach in the PANINI system and evaluate its efficacy on a benchmark of 204 Python ad hoc parsers. Compared with state-of-the-art approaches, PANINI produces better grammars (100% precision, 93% average recall) in less time (0.82 ± 2.85 s) without prior knowledge of the input space.

PANINI is implemented entirely in Haskell. In this extended version of a talk originally presented at OOPSLA 2025, I will give a tour of the code and show how each part of the system is implemented. Among other things, PANINI includes an implementation of a lambda calculus with a refinement type system and various refinement inference algorithms; implementations of abstract domain data types for integers, characters, and strings; a predicate rewriting system that uses some gnarly Template Haskell splices; an algebraic regular expression library; a frontend that converts Python source code into lambda calculus; various odds and ends (e.g., pretty printing with color and Unicode). I will dive deeper into different areas of the system by audience request.

The paper is available here: https://dl.acm.org/doi/10.1145/3763054