Two papers at HATRA

Today my students Gan Shen and Patrick Redmond and I are (virtually) attending the HATRA workshop co-located with SPLASH. HATRA is a relatively new workshop, focusing on human factors in the design of type systems and program reasoning assistants. It’s my first time at HATRA, and I’m enjoying it so far!

My students will be presenting two papers at HATRA (in back-to-back talks!): Patrick will present “Toward Hole-Driven Development with Liquid Haskell”, co-authored by Gan and me, and Gan will present “Toward SMT-based Refinement Types in Agda”, which I co-authored. Very roughly speaking, Patrick’s presentation will be about making Liquid Haskell more like Agda, and Gan’s will be about making Agda more like Liquid Haskell!

Making Liquid Haskell more like Agda

Liquid Haskell is an extension to the Haskell programming language that adds support for refinement types: data types augmented with SMT-decidable logical predicates that refine the set of values that can inhabit a type. While Liquid Haskell was originally intended for “lightweight” (i.e., fully automated and decidable, like most type checkers) program verification, the recent additions of refinement reflection and proof combinators make it possible to use Liquid Haskell for general-purpose mechanized theorem proving, where the human can assist the SMT solver to prove properties it couldn’t prove on its own. A growing list of large-scale mechanized proof developments in Liquid Haskell take advantage of these capabilities.

Liquid Haskell has a lot going for it as a verification platform. To me, the best part is that you can directly verify real, executable Haskell programs, just by writing Haskell! Unfortunately, the Liquid Haskell proof development experience lags behind more established proof assistants like Agda or Coq. Liquid Haskell provides only coarse-grained feedback to the user — either it reports a type error, or it doesn’t. There’s not (yet!) much support for interactive proof development. The feedback loop consists of trying to typecheck your code, making a change, and trying to typecheck it again.

In this paper, Patrick, Gan and I propose improving the usability of Liquid Haskell as a theorem prover by extending it with support for Agda-style typed holes and interactive editing commands that take advantage of them. In Agda, typed holes allow programmers to indicate unfinished parts of a proof, and incrementally complete the proof in a dialogue with the compiler. While GHC Haskell already has its own (Agda-inspired!) support for typed holes, we posit that typed holes would be especially powerful and useful if combined with Liquid Haskell’s refinement types and SMT automation. We discuss how typed holes might work in Liquid Haskell, and we consider possible implementation approaches and next steps.

Making Agda more like Liquid Haskell

Agda is a dependently-typed programming language in which types can depend on terms. Using dependent types, we can encode rich, precise properties of programs using types and prove that those properties hold at compile time through type checking. Dependent types offer great versatility and power, but developing proofs with them can be tedious and requires considerable human guidance. In our paper, we give the example of a Fin n type, the type of natural numbers less than n. For instance, 0, 1, and 2 are all terms that inhabit the type Fin 3. Any term that inhabits Fin 2 also inhabits Fin 3 — in other words, the former is a subtype of the latter, and so a term of type Fin 2 should be usable in any context where a term of type Fin 3 is well-typed — but Agda’s type checker doesn’t think so, and requires us to painstakingly construct a new term of the desired type.

We can address this usability issue in two stages. First, we observe that a value of type Fin n can be expressed as a pair of a number m and a proof that m < n. In fact, Agda already has refinement types in its standard library that work like this. There’s still the issue of proving that any number less than n is also less than n + 1, though. Fortunately, tedious arithmetic proofs like this are where SMT solvers excel. So, we can call off to an SMT solver to automate filling in the proof component of the pair. In Agda, we can do this using the very cool Schmitty tool created by Wen Kokke. In fact, Gan and Wen recently extended Schmitty to support a theory of natural numbers, and if I’m not mistaken, Gan will be showing off that support in a live demo during his HATRA talk today!

A spectrum of interactive and automated theorem proving

Theorem-proving systems have historically fallen into two camps: interactive theorem proving, exemplified by proof assistants such as Agda, and automated theorem proving, exemplified by SMT solvers and tools that build on them. Each approach has its strengths and weaknesses, and the boundary between the two camps is blurred by hybrid automatic/interactive (sometimes called “auto-active”) verification approaches, with different tools providing varying degrees of granularity of feedback provided to the human user, and different styles of specifying program properties. Liquid Haskell represents one point in this design space, as do emerging proof assistants that integrate SMT automation such as Lean and F*; a version of Agda augmented with SMT-based refinement types would, too. In the long run, we hope to not only explore individual points in the space, but systematically survey the landscape of such hybrid tools and contribute to a holistic scientific understanding of the space.