Toward Hole-Driven Development in Liquid Haskell

Refinement types (Rushby et al., 1998; Xi and Pfenning, 1998) let programmers specify data types augmented with logical predicates, called refinement predicates, that restrict the set of values that can inhabit the type. Depending on the expressivity of the language of refinement predicates, programmers can specify rich program properties using refinement types, sometimes at the expense of the decidability of type checking. Liquid Haskell avoids that problem by restricting refinement predicates to an SMT-decidable logic (Rondon et al., 2008; Vazou et al., 2014). For example, in Liquid Haskell we could define the type of even integers by refining the Haskell type v:Int — v mod 2 == 0 , where v:Int binds the name Int that appear in the refinement predicate. One could define an analogous refinement type for odd integers, and then write a Liquid Haskell function for adding them:

The type oddAdd expresses the precondition that y will be odd, and the return type postcondition that de-moura-z3. If the solver finds a verification condition to be invalid, typechecking fails. If the return type of OddInt, for instance, the above code would fail to typecheck. Aside from preconditions and postconditions of individual functions, Liquid Haskell makes it possible to verify extrinsic properties that are not specific to any particular function’s definition. For example, the type of mintedhaskell sumOdd :: x : OddInt -¿ y : EvenInt -¿ _:Proof — (x + y) mod 2 == 1 sumOdd __= () Here, proof that the sum of y is odd. (In Liquid Haskell, () (unit) type, but refined with constraints that express the property we wish to prove.) Because the proof of this particular property is easy for the SMT solver to carry out automatically, the body of the (), the sole inhabitant of the unit type. In general, however, programmers can specify arbitrary extrinsic properties in refinement types, including properties that refer to arbitrary Haskell functions via refinement reflection (Vazou et al., 2017b). The programmer can then prove those extrinsic properties by writing Haskell programs that inhabit those refinement types, using Liquid Haskell’s provided proof combinators — with the help of the underlying SMT solver to simplify the construction of these proofs-as-programs (Vazou et al., 2018, 2017b). Liquid Haskell thus occupies a unique position at the intersection of SMT-based program verifiers such as Dafny (Leino, 2010), and proof assistants that leverage the Curry-Howard correspondence such as Coq and Agda. A Liquid Haskell program can consist of both application code like sumOdd (which only “runs” at compile time), but, pleasantly, both are just Haskell programs, albeit annotated with refinement types. Being based on Haskell enables programmers to gradually port code from vanilla Haskell to Liquid Haskell, adding richer specifications to code as they go. Furthermore, verified Liquid Haskell libraries can be used directly in arbitrary Haskell programs, letting programmers take advantage of formally-verified components from unverified code written in an industrial-strength, general-purpose language. Finally, unlike Coq or Agda, which require an executable implementation to be extracted from the code written in the proof assistant’s vernacular language, Liquid Haskell enables proving properties both in and about the code to be executed, resulting in immediately executable verified code with no need for a further extraction step.

As a simple mock-up of how typed holes might work in Liquid Haskell, consider a len. One way to state this property is as an intrinsic property on the type of mintedhaskell listLength :: xs:_-¿ v : Nat — v == len xs listLength [] = _0 listLength (y:ys) = 1 + _1 Here, _1 are holes, indicating that the programmer needs help filling in these parts of the code. Given the refinement type annotation on xs == [] in this case, we could expect that the type checker would be able to tell us that the type of the first hole is v : Nat — 1 + v == len (y:ys) , but the type checker should be able to take advantage of the underlying SMT solver’s automated reasoning about linear arithmetic to conclude that the type of the second hole is mintedhaskell _0 : v : Nat — v == len [] _1 : v : Nat — v == len (y:ys) - 1 which can be further simplified to

at which point we know we need listLength ys for _1 respectively. The preceding example shows how a programmer might use typed holes for writing code with intrinsic refinement type specifications, but how about for writing extrinsic proofs? Instead of giving a refinement type to listLength and mintedhaskell listLength :: [a] -¿ Nat listLength [] = 0 listLength (y:ys) = 1 + listLength ys listLengthProof :: xs:_-¿ _:Proof — listLength xs == len xs listLengthProof = _0 The body of _0. When we attempt to compile this code, since the property we are trying to show relates the return values of len, Liquid Haskell might start by suggesting a case split on one of the functions:

Found hole ‘_0 of type ‘xs:[a] -> { _:Proof | listLength xs == len xs }.
       Consider a case split as in the body of ‘listLength.

The case split could be automated with a keystroke, or manually completed. In either case, the result is a partially completed proof with two holes:

The first hole, _:Proof — listLength xs == len xs . In [] in place of listLength xs and then evaluate the call to 0, with similar steps to evaluate 0, to complete the proof. This process could be automated after Liquid Haskell encounters the hole by checking whether verbatim Found hole ‘_0’ of type ‘ _:Proof — xs == [] & listLength xs == len xs ’. This can be completed with ‘()’. The replacement of () could again be automated with a keystroke, or manually completed. Even better, completing branches with () or a new hole, according to whether more work is needed. The second hole, _:Proof — listLength xs == len xs . In (y:ys) in place of listLength xs and then evaluate the call to 1 + listLength ys, with similar steps for _:Proof — 1 + listLength ys == 1 + len ys. This could be automated after Liquid Haskell encounters the hole and finds that replacing it with verbatim Found hole ‘_1’ of type ‘ _:Proof — xs == (y:ys) & listLength xs == len xs ’. Conclusion expands to ‘1 + listLength ys == 1 + len ys’, which is simplified to ‘listLength ys == len ys‘. This message does not suggest any action directly, but it does show us an intermediate goal which if proved would be sufficient to show the overall conclusion inductive assumption. Replacing listLengthProof ys could potentially be automated with a keystroke in this simple example, although it is unlikely to be quite this obvious in nontrivial proofs.