Type Systems & Mechanized Proofs

Problem. Two notations dominate effectful code and each gives up half of what you need. do-notation embeds any monad, but monads chain everything into one sequence, discarding parallelism that was there for the taking. Idiom brackets embed applicatives, which run in parallel, but cannot express one effect depending on another’s result. Real programs are neither purely sequential nor purely parallel, and composing the two was an open problem. Worse, both notations impose a rigid shape on the code (one effect per line), rather than letting effects appear where they are actually used.

Idea. A mixed applicative/monadic notation written in direct style. A purify block introduces an operator ↓ : F[X] ⇒ X, and where you write it is all the compiler needs: parallelism is read off the structure of the code rather than recovered afterwards from a sequential program. Arguments of ++ cannot depend on each other, so they run in parallel; a fetch whose URL comes from another fetch cannot, so it does not.

Result. A one-pass translation from direct style to effect combinators, proved to preserve typability, semantics and parallelism. Parallelism is made precise as the span of a term (the longest chain of effectful operations) against its work (the total number of them); the translation is span-preserving, which notations built on monads alone cannot be. The proof is mechanized in Coq using parametric higher-order abstract syntax, and the translation is implemented in Scala via macros, staying close to the formal development. Distinguished Paper and Distinguished Artifact at ECOOP 2023.

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

Problem. Dependently typed languages lean on Miller pattern unification, a well-behaved fragment of the undecidable general problem. But that fragment has a blunt limitation: it cannot synthesize a function defined by case analysis. The constraint system F true = 1, F false = 2 is trivial to any functional programmer (the answer is a match), yet it falls outside Miller patterns and outside the modern extensions too (FCU, DHOP), all of which reject metavariables applied to terms that are not variables.

Idea. These constraints are not exotic; they come straight out of type inference over eliminators. Omit the motive P of an induction principle and the checker is immediately asked to solve P true = ℕ, P false = Bool, again a definition by cases. That correspondence is the whole point: such constraints are definitions by dependent pattern matching. So bring pattern matching into unification itself, collecting delayed constraints and discharging them with a pattern matching compiler.

Result. A prototype dependently typed language (under 3000 lines of Lean) that collects the constraints falling outside the pattern fragment, suspends them as delayed problems, and hands them to a dependent pattern matching compiler: the metavariable becomes a function symbol, its arguments become pattern variables, and the constraint states the desired output. It infers solutions that Rocq and Lean reject, pointing toward a unification procedure that merges type inference with pattern matching compilation. An extended abstract.

Links: arxiv

Problem. Formally verifying choreographies in a proof assistant is notoriously painful, because most choreographic languages are functional (receiving a message introduces a fresh variable), and machine-checked proofs about variable binding and substitution end up dominating the whole effort.

Idea. Give every participant a local state of an arbitrary type, and model “receive a message” not as binding a new variable, but as a plain function from (old state, message) to new state (a state transformer). Receiving a message then introduces no binder at all.

Result. A full mechanization (in Lean) proving soundness and completeness of endpoint projection, deadlock freedom, confluence, and a Hoare logic for choreographies, sidestepping the binding and substitution reasoning that usually dominates such a development.

Links: arxiv

Problem. Choreographic libraries embedded in a host language (Haskell, Rust, …) still have a gap: a “located” value that a role may or may not own is modelled as an option type, and unwrapping it always keeps a dead “impossible” branch (ruled out only by the library author’s discipline, never by the type checker).

Idea. In a dependently-typed host language, make “this role owns this value” a genuine machine-checked proof rather than a runtime tag: a located value’s type carries a proof that the current role is among its owners.

Result. A choreographic library where no error/undefined appears anywhere in the core implementation: totality is enforced by the compiler itself, without sacrificing expressivity relative to prior, partial libraries.

Links: arxiv