When indexing into a vector, you usually have one of two options:

- enable bounds-checking to throw an exception if you index out of bounds or:
- disable bounds-checking to improve performance.

Both of these options are still unsatisfactory, though. Even if your program fails fast with an exception, your program still failed.

Fortunately, Haskell programmers can now select a third option:

- verify at compile time that you never index a vector out of bounds.

A new tool named Liquid Haskell makes this sort of verification possible. Liquid Haskell is a customizable static analysis tool for the Haskell language that eliminates a wide variety of programming errors at compile time that would normally be difficult to eliminate using Haskell's ordinary type system.

However, the Liquid Haskell tool still needs a lot of polish. I've been using Liquid Haskell for the last couple of months and in my experience the tool is just starting to become "usable in anger". I'm saying this as somebody who has reported eight issues with the tool so far and encountered a ninth issue while writing up this post.

I'll illustrate how Liquid Haskell works by:

- implementing a binary search algorithm for Haskell's
`Vector`

type, - using Liquid Haskell to statically verify the complete absence of out-of-bound indexing, and then:
- safely disabling bounds checking since I've proven the algorithm correct.

Along the way I'll highlight both the ups and downs of using Liquid Haskell so that you can preview what it's like to use the tool.

#### Binary search

Let's begin with the following Haskell code for binary search over a sorted `Vector`

. I've included a real mistake I made when first implementing this algorithm. See if you can spot the mistake:

```
import Data.Vector as Vector
{-| Postconditions:
* If the result is `Just i`, then `0 <= i < length v`
-}
binarySearch :: Ord a => a -> Vector a -> Maybe Int
binarySearch x v = loop x v 0 (Vector.length v - 1)
{-| Preconditions:
* `0 <= lo < length v`
* `lo <= hi < length v`
-}
loop :: Ord a => a -> Vector a -> Int -> Int -> Maybe Int
loop x v lo hi = do
let mid = (lo + hi) `div` 2
if x < v ! mid
then do
let hi' = mid - 1
if lo <= hi'
then loop x v lo hi'
else Nothing
else if v ! mid < x
then do
let lo' = mid + 1
if lo' <= hi
then loop x v lo' hi
else Nothing
else Just mid
```

Let's try this out on a few values:

```
$ stack ghci --resolver=lts-3.19 vector
...
Prelude> :load binarysearch.hs
...
*Main> let v = Vector.fromList [1, 4, 5, 10]
*Main> binarySearch 4 v
Just 1
*Main> binarySearch 3 v
Nothing
*Main> binarySearch 1 v
Just 0
*Main> binarySearch 0 v
Nothing
*Main> binarySearch 10 v
Just 3
*Main> binarySearch 11 v
Nothing
```

#### Liquid Haskell

We can run this code through the Liquid Haskell tool in order to locate all potential out-of-bounds indexes. In order to install the tool we must have some SMT solver on our `$PATH`

which Liquid Haskell uses to automate the deduction process. In my case, I installed the Z3 solver by downloading the latest stable release from this page (Version 4.4.1 at the time of this writing):

Then I installed Liquid Haskell using `stack`

:

```
$ cat stack.yaml
resolver: lts-3.19
packages: []
extra-deps:
- intern-0.9.1.4
- liquid-fixpoint-0.4.0.0
$ stack build liquidhaskell
```

... and then I run the `liquid`

tool over my code like this:

```
$ stack exec liquid binarysearch.hs
LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.
**** DONE: Extracted Core using GHC *******************************************
**** DONE: generateConstraints ************************************************
**** START: fixpoint ***********************************************************
========================================================
© Copyright 2009 Regents of the University of California.
All Rights Reserved.
========================================================
............../Unsatisfied Constraints:
{snip}
UNSAT
**** DONE: fixpoint ***********************************************************
**** DONE: solve **************************************************************
**** DONE: annotate ***********************************************************
**** UNSAFE ********************************************************************
binarysearch.hs:18:16-18: Error: Liquid Type Mismatch
Inferred type
VV : {VV : Int | VV == mid}
not a subtype of Required type
VV : {VV : Int | VV >= 0 && VV < vlen v}
In Context
VV : {VV : Int | VV == mid}
v : {v : (Vector a) | 0 <= vlen v}
?a : {?a : Int | ?a == lo + hi}
hi : Int
mid : {mid : Int | mid == ?a / ?b && (?a >= 0 && ?b >= 0 => mid >= 0) &&
(?a >= 0 && ?b >= 1 => mid <= ?a)}
?b : {?b : Int | ?b == 2}
lo : Int
binarysearch.hs:22:23-24: Error: Liquid Type Mismatch
Inferred type
VV : {VV : Int | VV == lo}
not a subtype of Required type
VV : {VV : Int | VV < lo && VV >= 0}
In Context
VV : {VV : Int | VV == lo}
lo : Int
binarysearch.hs:24:17-19: Error: Liquid Type Mismatch
Inferred type
VV : {VV : Int | VV == mid}
not a subtype of Required type
VV : {VV : Int | VV >= 0 && VV < vlen v}
In Context
VV : {VV : Int | VV == mid}
v : {v : (Vector a) | 0 <= vlen v}
?a : {?a : Int | ?a == lo + hi}
hi : Int
mid : {mid : Int | mid == ?a / ?b && (?a >= 0 && ?b >= 0 => mid >= 0) &&
(?a >= 0 && ?b >= 1 => mid <= ?a)}
?b : {?b : Int | ?b == 2}
lo : Int
binarysearch.hs:28:23-25: Error: Liquid Type Mismatch
Inferred type
VV : {VV : Int | VV == lo'}
not a subtype of Required type
VV : {VV : Int | VV < lo && VV >= 0}
In Context
VV : {VV : Int | VV == lo'}
?a : {?a : Int | ?a == lo + hi}
?c : {?c : Int | ?c == 2}
hi : Int
mid : {mid : Int | mid == ?a / ?c && (?a >= 0 && ?c >= 0 => mid >= 0) &&
(?a >= 0 && ?c >= 1 => mid <= ?a)}
?b : {?b : Int | ?b == 1}
lo : Int
lo' : {lo' : Int | lo' == mid + ?b}
```

Okay, so we got four errors on our first check. How concerned should we be?

Usually these errors fall into three categories:

Missing preconditions

We fix these by formally documenting the preconditions of our own functions using Liquid Haskell's type system

Missing postconditions

We fix these by formally documenting the postconditions of functions we use, also using Liquid Haskell's type system

Genuine bugs (i.e. your code is wrong even when all preconditions and postconditions are correctly documented)

We fix these by correcting our code

When we first begin most of the errors will fall into the first two categories (missing preconditions or postconditions) and as things progress we may discover errors in the third category (genuine bugs).

#### Preconditions

Liquid Haskell documents the preconditions and postconditions of many Haskell functions "out-of-the-box" by providing "refined" type signatures for these functions. You can find all of the built-in refined type signatures here:

... and here's an example refined type from the `Data.Vector`

module (slightly modified from the original):

`assume ! :: v : Vector a -> { i : Int | 0 <= i && i < vlen v } -> a`

`(!)`

is Haskell's infix operator for indexing into a vector. Normally, the ordinary Haskell type signature for this operator would look like this:

`(!) :: Vector a -> Int -> a`

... which you can read roughly as saying: "The first (left) argument to this infix operator is a `Vector`

containing elements of type `a`

(where `a`

can be any type). The second (right) argument to this infix operator is the index you want to retrieve. The result is the retrieved element.

Here is an example use of the operator:

```
$ stack ghci --resolver=lts-3.19 vector
Prelude> import Data.Vector as Vector
Prelude Vector> let v = Vector.fromList [1, 4, 5, 10]
Prelude Vector> v ! 0
1
Prelude Vector> v ! 3
10
Prelude Vector> v ! 2
5
Prelude Vector> v ! 4
*** Exception: ./Data/Vector/Generic.hs:249 ((!)): index out of bounds (4,4)
```

Oops! This operator is not safe because indexing can fail at runtime with an exception if you index out of bounds.

This is where Liquid Haskell comes into play. Liquid Haskell lets you write richer type signatures that document preconditions and postconditions. These type signatures resemble Haskell type signatures except that you can decorate them with logical predicates, like this:

`assume ! :: v : Vector a -> { i : Int | 0 <= i && i < vlen v } -> a`

This is an example of a **precondition**. The above refined type says: "The index, `i`

, must be non-negative and must be less than the length of the vector, `v`

, that you supplied for the first argument".

So how does Liquid Haskell know what the length of the `vector`

is? Remember that Liquid Haskell needs to somehow verify this precondition at compile time even though we don't necessarily know what the input will be at compile time. In fact, Liquid Haskell actually doesn't know anything about `Vector`

s at all, let alone their lengths, unless we teach it!

#### Postconditions

We can teach Liquid Haskell about `Vector`

lengths by introducing a new "`measure`

" named `vlen`

:

`measure vlen :: Vector a -> Int`

The only thing we provide is the type of `vlen`

, but there is no code associated with `vlen`

. Just treat `vlen`

as an abstract type-level placeholder for the length of the `Vector`

. We can use `vlen`

to give a more refined type to `Vector.length`

:

`assume Vector.length :: v : Vector a -> { n : Int | n == vlen v }`

This is an example of a **postcondition**. You can read this type signature as saying: "We know for sure that whatever `Int`

that `length`

returns must be the length of the `Vector`

".

The `assume`

keyword indicates that we haven't proven this the correctness of this refined type. Instead we are asserting that the type is true. Any time you study a Liquid Haskell program you need to stare really hard at any part of the code that uses `assume`

since that's an escape hatch that might compromise any safety guarantees.

Not all postconditions require the use of `assume`

. In fact, Liquid Haskell can automatically promote a restricted subset of Haskell safely to the type level. Unfortunately, this subset does not include operations on `Vector`

s, which is why we must assert the correctness of the above refined type.

#### Safety

Let's verify that the refined types for `(!)`

and `length`

work correctly using a small test example. We'll begin with a program that is not necessarily safe:

```
import Data.Vector as Vector
example :: Vector a -> a
example v = v ! 2
```

We run the above program through the `liquid`

type-checker and get a type error (as expected) since the type-checker cannot verify that the input `Vector`

has at least three elements:

```
$ stack exec example.hs
...
UNSAT
**** UNSAFE ********************************************************************
safe.hs:4:17: Error: Liquid Type Mismatch
Inferred type
VV : {VV : Int | VV == ?a}
not a subtype of Required type
VV : {VV : Int | VV >= 0 && VV < vlen v}
In Context
VV : {VV : Int | VV == ?a}
v : {v : (Vector a) | 0 <= vlen v}
?a : {?a : Int | ?a == 2}
```

Don't worry if you don't understand the type error just yet. Right now all we care about is the line and column number, which point directly at the `2`

in the source code:

```
import Data.Vector as Vector
example :: Vector a -> a
example v = v ! 2
-- ERROR HERE ^
```

There are two ways we can fix our program. The best solution is to add a precondition to the type of our `example`

function. We can specify that our function only works for `Vector`

s that have at least 3 elements:

```
import Data.Vector as Vector
{-@ example :: { v : Vector a | 3 <= vlen v } -> a @-}
example :: Vector a -> a
example v = v ! 2
```

We document this in a second parallel type signature embedded within a Haskell comment. Liquid Haskell is designed to be backwards compatible with the Haskell language and is not yet a formal language extension supported by `ghc`

, which is why Liquid Haskell types have to live inside comments.

Once we add that precondition then the `liquid`

Haskell type-checker verifies that our program is correct:

```
$ stack exec liquid example.hs
...
SAT
**** DONE: fixpoint ***********************************************************
**** DONE: solve **************************************************************
**** DONE: annotate ***********************************************************
**** SAFE **********************************************************************
```

WARNING: Once you begin using this tool you will quickly grow addicted to that `SAFE`

message. Using Liquid Haskell feels very much like a fun game where the reward is correct code!

Another way we can satisfy the type-checker is to check the `Vector`

's length at runtime and return `Nothing`

if the `Vector`

is too small. We wrap successful results in `Just`

if the `Vector`

is large enough:

```
import Data.Vector as Vector
example :: Vector a -> Maybe a
example v =
if 3 <= Vector.length v
then Just (v ! 2)
else Nothing
```

Notice how this program requires no Liquid Haskell type signature or type annotation. Liquid Haskell is smart enough to figure out that the precondition for `(!)`

was already satisfied by the runtime check:

```
$ stack exec liquid example.hs
...
**** SAFE **********************************************************************
```

However, we prefer to avoid runtime checks if possible. Type-level refinements improve on runtime checks in two important ways:

- Refinements are "free" - they incur no runtime cost
- Refinements encourage pushing fixes upstream (by constraining the input) instead of propagating problems downstream (by returning a
`Maybe`

output)

#### Binary search - Continued

Let's revisit our binary search algorithm and study the first error message more closely:

```
binarysearch.hs:18:16-18: Error: Liquid Type Mismatch
Inferred type
VV : {VV : Int | VV == mid}
not a subtype of Required type
VV : {VV : Int | VV >= 0 && VV < vlen v}
In Context
VV : {VV : Int | VV == mid}
v : {v : (Vector a) | 0 <= vlen v}
?a : {?a : Int | ?a == lo + hi}
hi : Int
mid : {mid : Int | mid == ?a / ?b && (?a >= 0 && ?b >= 0 => mid >= 0) &&
(?a >= 0 && ?b >= 1 => mid <= ?a)}
?b : {?b : Int | ?b == 2}
lo : Int
```

Your first reflex should be to jump to the line and column numbers, which point to this location:

```
{-| Invariants:
* `0 <= lo < length v`
* `lo <= hi < length v`
-}
loop :: Ord a => a -> Vector a -> Int -> Int -> Maybe Int
loop x v lo hi = do
let mid = (lo + hi) `div` 2
if x < v ! mid
-- ^^^ ERROR HERE
then do
let hi' = mid - 1
if lo <= hi'
then loop x v lo hi'
else Nothing
else if v ! mid < x
then do
let lo' = mid + 1
if lo' <= hi
then loop x v lo' hi
else Nothing
else Just mid
```

This suggests that we provided an index that might be out of bounds and the error message confirms that:

```
Inferred type
VV : {VV : Int | VV == mid}
not a subtype of Required type
VV : {VV : Int | VV >= 0 && VV < vlen v}
```

This is Liquid Haskell's way of saying: "I can't prove that `mid`

is within the vector bounds". Liquid Haskell will even explain its reasoning process, showing what refinements were in scope for that expression:

```
In Context
VV : {VV : Int | VV == mid}
v : {v : (Vector a) | 0 <= vlen v}
?a : {?a : Int | ?a == lo + hi}
hi : Int
mid : {mid : Int | mid == ?a / ?b && (?a >= 0 && ?b >= 0 => mid >= 0) &&
(?a >= 0 && ?b >= 1 => mid <= ?a)}
?b : {?b : Int | ?b == 2}
lo : Int
```

This is an example of the first class of errors: missing preconditions. Liquid Haskell can't read our comment so Liquid Haskell has no way of knowing that `lo`

and `hi`

are within the vector bounds. Therefore, Liquid Haskell can't conclude that their midpoint, `mid`

, is also within the vector bounds.

This is very easy to fix. We can transform our unstructured comment describing preconditions into a refined type for the `loop`

function:

```
{-@
loop
:: Ord a
=> x : a
-> v : Vector a
-> lo : { lo : Int | 0 <= lo && lo < vlen v }
-> hi : { hi : Int | lo <= hi && hi < vlen v }
-> Maybe Int
@-}
loop :: Ord a => a -> Vector a -> Int -> Int -> Maybe Int
```

Now our documentation is machine-checked and will never go out of date!

#### Refining our input

Now we get several new errors when we run our code through the `liquid`

type-checker. I've only included the first error message for brevity:

```
binarysearch.hs:8:29: Error: Liquid Type Mismatch
Inferred type
VV : {VV : Int | VV == ?a}
not a subtype of Required type
VV : {VV : Int | 0 <= VV && VV < vlen v}
In Context
VV : {VV : Int | VV == ?a}
v : {v : (Vector a) | 0 <= vlen v}
?a : {?a : Int | ?a == 0}
```

This points to a new subexpression:

```
binarySearch :: Ord a => a -> Vector a -> Maybe Int
binarySearch x v = loop x v 0 (Vector.length v - 1)
-- ERROR HERE ^
```

Liquid Haskell incorporated the new information we supplied through the refined type. The type-checker then worked backwards from `loop`

's preconditions and found a problem in our code via the following reasoning process:

- The type of
`loop`

says that the`lo`

argument must be less than the length of the vector - We supplied
`0`

for the`lo`

argument to`loop`

- Therefore the
`Vector`

`v`

needs to be at least length`1`

- But we never proved that the
`Vector`

has at least one element!

This is an example of the third class of errors: a genuine bug. I introduced this bug when I first wrote up this algorithm and Liquid Haskell caught my mistake. I never thought about the case where the `Vector`

was empty. Many programmers smarter than me would carefully consider the corner case where the `Vector`

was empty, but I use tools like Liquid Haskell so that I don't need to be smart (or careful).

In this case we don't want to refine the type of `binarySearch`

to require non-empty `Vector`

inputs since we want to support binary searches for `Vector`

s of all sizes. Instead, we will add a special case to handle an empty `Vector`

input:

```
binarySearch :: Ord a => a -> Vector a -> Maybe Int
binarySearch x v =
if Vector.length v == 0
then Nothing
else loop x v 0 (Vector.length v - 1)
```

#### Refining our output

Now the type-checker gives a new error message:

```
binarysearch.hs:25:16-18: Error: Liquid Type Mismatch
Inferred type
VV : {VV : Int | VV == mid}
not a subtype of Required type
VV : {VV : Int | VV >= 0 && VV < vlen v}
In Context
VV : {VV : Int | VV == mid}
v : {v : (Vector a) | 0 <= vlen v}
?a : {?a : Int | ?a == lo + hi}
hi : {hi : Int | lo <= hi && hi < vlen v}
mid : {mid : Int | mid == ?a / ?b && (?a >= 0 && ?b >= 0 => mid >= 0) &&
(?a >= 0 && ?b >= 1 => mid <= ?a)}
lo : {lo : Int | 0 <= lo && lo < vlen v}
?b : {?b : Int | ?b == 2}
```

Let's see where this points:

```
loop :: Ord a => a -> Vector a -> Int -> Int -> Maybe Int
loop x v lo hi = do
let mid = (lo + hi) `div` 2
if x < v ! mid
-- ^^^ ERROR HERE
then do
let hi' = mid - 1
if lo <= hi'
then loop x v lo hi'
else Nothing
else if v ! mid < x
then do
let lo' = mid + 1
if lo' <= hi
then loop x v lo' hi
else Nothing
else Just mid
```

This is the same as the first error message! WHAT GIVES?!?!

Liquid Haskell already knows that both `lo`

and `hi`

are within the `Vector`

bounds, but cannot deduce that their midpoint must also lie within the `Vector`

bounds.

This is an example of the second class of errors: missing postconditions. ~~In this case the issue here is a deficiency of Liquid Haskell's built-in Prelude. Without going into too many details, the built-in refinement for the ~~`div`

function uses integer division, but for some reason type-level division does not provide sufficient information for Liquid Haskell to deduce that the midpoint lies between `lo`

and `hi`

. I'm actually still in the process of narrowing downthe precise problem before reporting this on the Liquid Haskell issue tracker, so I may be interpreting this problem incorrectly.

Edit: Rhanjit Jhala explained that you can fix this by supplying the `--real`

flag or adding this pragma to the top of the file:

```
{-@ LIQUID "--real" @-}
import Data.Vector as Vector
...
```

Once you supply this flag then the postcondition for `div`

correctly satisfies the type-checker. The previous version of this post used an `assume`

to enforce the relevant postcondition, which is no longer necessary with this flag.

#### Termination checking

We're now down to two error messages, the first of which is:

```
binarysearch.hs:31:23-24: Error: Liquid Type Mismatch
Inferred type
VV : {VV : Int | VV == lo}
not a subtype of Required type
VV : {VV : Int | 0 <= VV && VV < vlen v && VV < lo && VV >= 0}
In Context
VV : {VV : Int | VV == lo}
v : {v : (Vector a) | 0 <= vlen v}
lo : {lo : Int | 0 <= lo && lo < vlen v}
```

This one took me an hour to figure out and the error message originates from Liquid Haskell's termination checker! I only figured this error out because I already knew that Liquid Haskell had a built-in termination checker and even then I had to first minimize the code example before I fully understood the problem.

Liquid Haskell supports termination checking by default, which is actually pretty awesome despite the confusing error. Termination checking means that Liquid Haskell verifies that our code never endlessly loops. Or in other words, Liquid Haskell transforms Haskell into a "total" programming language (i.e. a programming language where computation always halts). You can also disable the termination checker completely or disable the checker for selected functions if you find the check too restrictive.

The termination checker proves termination by looking for some sort of "well-founded metric" that shows that the function will eventually terminate. This "well-founded metric" is usually an `Int`

that decreases each time the function recurses and the recursion halts when the `Int`

reaches `0`

.

By default, Liquid Haskell guesses and tries to use the first `Int`

argument to the recursive function as the well-founded metric, which was the `lo`

argument in our example. You get an error message like the above when Liquid Haskell guesses wrong. In our case, `lo`

is not a suitable "well-founded" metric because `lo`

does not decrease every time the function recurses. Quite the opposite: `lo`

either stays the same or increases.

```
loop x v lo hi = do
let mid = (lo + hi) `div` 2
if x < v ! mid
then do
let hi' = mid - 1
if lo <= hi'
then loop x v lo hi' -- `lo` stays the same
else Nothing
else if v ! mid < x
then do
let lo' = mid + 1
if lo' <= hi
then loop x v lo' hi -- `lo` increases
else Nothing
else Just mid
```

The `hi`

argument is also not a suitable well-founded metric. `hi`

never increases, but `hi`

does not necessarily decrease either:

```
loop x v lo hi = do
let mid = (lo + hi) `div` 2
if x < v ! mid
then do
let hi' = mid - 1
if lo <= hi'
then loop x v lo hi' -- `hi` decreases
else Nothing
else if v ! mid < x
then do
let lo' = mid + 1
if lo' <= hi
then loop x v lo' hi -- `hi` stays the same
else Nothing
else Just mid
```

However, we are not limited to using arguments as well-founded metrics. We can create our own custom metric that is a composite of the given arguments. In this case we **do** know that `hi - lo`

always decreases on every iteration and we can instruct Liquid Haskell to use that as the well-founded metric using the following syntax:

```
{-@
loop
:: Ord a
=> x : a
-> v : Vector a
-> lo : { lo : Int | 0 <= lo && lo < vlen v }
-> hi : { hi : Int | lo <= hi && hi < vlen v }
-> Maybe Int
/ [hi - lo] -- The well-founded metric
@-}
```

#### SAFE

Once we add the well-founded metric the type-checker accepts our program!!!

```
stack exec liquid binarysearch.hs
LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.
**** DONE: Extracted Core using GHC *******************************************
**** DONE: generateConstraints ************************************************
**** START: fixpoint ***********************************************************
========================================================
© Copyright 2009 Regents of the University of California.
All Rights Reserved.
========================================================
........................../
SAT
**** DONE: fixpoint ***********************************************************
**** DONE: solve **************************************************************
**** DONE: annotate ***********************************************************
**** SAFE **********************************************************************
```

That's it! We're done. Liquid Haskell analyzed the flow of our program and statically verified two properties about our program:

- Our program will never fail from an out-of-bounds index error
- Our program will never loop endlessly

The only assistance we had to provide was to document preconditions and postconditions in the types and the type-checker automated the rest of the proof.

This means that we can safely disable bounds checking by replacing `(!)`

with `Vector.unsafeIndex`

. Compile-time memory safety already rocks, but getting a free speed improvement is icing on the cake.

Edit: /u/f2u on /r/haskell points out that there is still a bug: the code can fail due to integer overflow.

You can further eliminate the possibility of integer overflow through the use of refinement types, but Liquid Haskell does not provide these extra refinements to protect against overflow by default. Instead you must opt-in to them by adding your own refinements.

The solution to prevent overflow is to replace this:

`(lo + hi) `div` 2`

... with this:

`lo + (hi - lo) `div` 2`

#### Exercise

If you remember correctly, our original code had a postcondition:

```
{-| Postconditions:
* If the result is `Just i`, then `0 <= i < length v`
-}
binarySearch :: Ord a => a -> Vector a -> Maybe Int
binarySearch x v = loop x v 0 (Vector.length v - 1)
```

Try modifying the final code example (See the `Appendix`

) to add this postcondition as a refinement to the type of `binarySearch`

. **Hint:** you will also need to further refine the type of `loop`

as well.

You will not need to `assume`

any additional information if you do this correctly. The type-checker should be able to verify the newly added postcondition from the existing preconditions.

#### Conclusion

If you would like to learn more about Liquid Haskell, I highly recommend the official Liquid Haskell tutorial. This tutorial is well-written, comprehensive, and packed with practical examples:

Liquid Haskell is designed in the same spirit as Haskell: check as much as possible with as little input from the programmer. Despite all the bugs I run into, I keep coming back to this tool because of the very high power-to-weight ratio for formal verification.

Also note that the final program is still valid Haskell code so we don't sacrifice any compatibility with the existing Haskell toolchain by using Liquid Haskell.

#### Appendix

Here is the complete final program that type-checked, for reference:

```
{-@ LIQUID "--real" @-}
import Data.Vector as Vector
{-| Postconditions:
* If the result is `Just i`, then `0 <= i < length v`
-}
binarySearch :: Ord a => a -> Vector a -> Maybe Int
binarySearch x v =
if Vector.length v == 0
then Nothing
else loop x v 0 (Vector.length v - 1)
{-@
loop
:: Ord a
=> x : a
-> v : Vector a
-> lo : { lo : Int | 0 <= lo && lo < vlen v }
-> hi : { hi : Int | lo <= hi && hi < vlen v }
-> Maybe Int
/ [hi - lo]
@-}
loop :: Ord a => a -> Vector a -> Int -> Int -> Maybe Int
loop x v lo hi = do
let mid = (lo + hi) `div` 2
if x < v ! mid
then do
let hi' = mid - 1
if lo <= hi'
then loop x v lo hi'
else Nothing
else if v ! mid < x
then do
let lo' = mid + 1
if lo' <= hi
then loop x v lo' hi
else Nothing
else Just mid
```

Thanks for the superb writeup Gabriel! To get rid of the `assume` for `midpoint`, add the `{-@ LIQUID "--real" @-}` pragma, which uses proper division. With it, in fact, you don't need a signature for `midpoint`, and can even just inline it:

ReplyDeletehttps://github.com/ucsd-progsys/liquidhaskell/blob/master/tests/pos/BinarySearch.hs

Thanks! I updated the post with the fix using the `--real` flag instead of an `assume`

DeleteGreat article, thanks! It's nice to see that Liquid Haskell is still alive.

ReplyDelete