Effects & Type Theory

← Back to Home

Notations and type checkers that let programmers write what they mean, and still check it.

A type system is a negotiation. The programmer wants to write what they mean; the compiler wants a guarantee it can actually check. Push too hard on the guarantee and the notation turns rigid (effects marshalled one per line, motives spelled out by hand). Push too hard on convenience and the guarantee evaporates. My work tries to move that boundary rather than pick a side:

  • Notation: writing effects in direct style, so that the structure of the code reveals which parts may run in parallel (ECOOP'23).
  • Inference: solving unification constraints that today’s proof assistants reject, such as an omitted induction motive, with Timon Böhler (TyDe'26).
  • Compilation: more precise monomorphization for first-class polymorphism (work in progress).
Highlight
  • 🏅 Distinguished Paper🏅 Distinguished Artifact A Direct-Style Effect Notation, ECOOP 2023
Collaborators
Timon Böhler Iurii Khosoi Mira Mezini Pascal Weisenburger

Timeline

2023ECOOP

A Direct-Style Effect Notation for Sequential and Parallel Programs

David Richter, Timon Böhler, Pascal Weisenburger, Mira Mezini

do-notation embeds monads but chains everything into one sequence; idiom brackets embed applicatives but cannot express one effect depending on another, and both force one effect per line. A purify block with a direct-style operator ↓ lets parallelism be read off the structure of the code. The one-pass translation to effect combinators is proved to preserve typing, semantics and parallelism (as the span of a term), mechanized in Coq, and implemented with Scala macros.

A dependency diagram: fetch(urlXX) and fetch(urlYY) start in parallel, each feeding a second fetch, and both chains converge on x ++ y
From the paper: the example's dependency structure (two independent chains, each internally sequential).

Links: ECOOP 2023 · paper · artifact · github · arxiv 🏅 Distinguished Paper🏅 Distinguished Artifact

2026TyDe @ FPW Paris · Extended abstract

From Pattern Unification Towards Pattern Matching Unification

David Richter, Timon Böhler

Miller pattern unification cannot synthesize a function defined by cases: F true = 1, F false = 2 falls outside it, yet such constraints arise as soon as the motive of an induction principle is omitted. Handing them to a dependent pattern matching compiler, a prototype in under 3000 lines of Lean infers solutions that Rocq and Lean reject.

The same induction-principle test in two languages: this work's prototype synthesizes the motive as a match on the Boolean, while Rocq fails with 'Unable to unify bool with ?P false'
Fig. 1 from the paper (excerpt): the litmus test, as this work's prototype and as Rocq handle it.

Links: arxiv

2026Work in progress (click to expand)

Increasing Precision in Monomorphization for First-Class Polymorphism

Iurii Khosoi, David Richter, Mira Mezini

Work in progress, building on Khosoi’s BSc thesis Monomorphization for System F (supervised by me). No preprint yet.

Open questions

Directions that come out of the work above, from thesis-sized (BSc/MSc) to PhD-scale:

  • More of the language in direct style. Loops and branches, and effect structures beyond monads and applicatives (selectives, comonads, arrows).
  • Recursive solutions. Letting unification synthesize recursive and mutually recursive functions, replacing the acyclicity check by a structural recursion check.
  • Integration. Compiling the resulting case trees into core terms and plugging them into an existing elaboration pipeline.

Useful background is functional programming and some Lean or Scala; my Type Systems lecture covers the foundations. If one of these interests you, write me an email.