# Bounding Vectors

Today, lets look at a classic use-case for refinement types, namely, the static verification of vector access bounds. Along the way, we'll see some examples that illustrate how LiquidHaskell reasons about recursion, higher-order functions, data types, and polymorphism.

```22: module VectorBounds (
23:     safeLookup
24:   , unsafeLookup, unsafeLookup'
25:   , absoluteSum, absoluteSum'
26:   , dotProduct
27:   , sparseProduct, sparseProduct'
28:   ) where
29:
30: import Prelude      hiding (length)
31: import Data.List    (foldl')
32: import Data.Vector  hiding (foldl')
```

## Specifying Bounds for Vectors¶

One classical use-case for refinement types is to verify the safety of accesses of arrays and vectors and such, by proving that the indices used in such accesses are within the vector bounds. Lets see how to do this with LiquidHaskell by writing a few short functions that manipulate vectors, in particular, those from the popular vector library.

First things first. Lets specify bounds safety by refining the types for the key functions exported by the module `Data.Vector`.

Specifications for `Data.Vector`

```50: module spec Data.Vector where
51:
52: import GHC.Base
53:
54: measure vlen  ::   (Vector a) -> Int
55: assume length :: x:(Vector a) -> {v:Int | v = (vlen x)}
56: assume !      :: x:(Vector a) -> {v:Int | 0 <= v && v < (vlen x)} -> a
```

In particular, we

• define a property called `vlen` which denotes the size of the vector,
• assume that the `length` function returns an integer equal to the vector's size, and
• assume that the lookup function `!` requires an index between `0` and the vector's size.

There are several things worth paying close attention to in the above snippet.

Measures

Recall that measures define auxiliary (or so-called ghost) properties of data values that are useful for specification and verification, but which don't actually exist at run-time. Thus, they will only appear in specifications, i.e. inside type refinements, but never inside code. Often we will use helper functions like `length` in this case, which pull or materialize the ghost values from the refinement world into the actual code world.

Assumes

We write `assume` because in this scenario we are not verifying the implementation of `Data.Vector`, we are simply using the properties of the library to verify client code. If we wanted to verify the library itself, we would ascribe the above types to the relevant functions in the Haskell source for `Data.Vector`.

Dependent Refinements

Notice that in the function type (e.g. for `length`) we have named the input parameter `x` so that we can refer to it in the output refinement.

In this case, the type

```91: assume length   :: x:(Vector a) -> {v : Int | v = (vlen x)}
```

states that the `Int` output is exactly equal to the size of the input `Vector` named `x`.

In other words, the output refinement depends on the input value, which crucially allows us to write properties that relate different program values.

Verifying a Simple Wrapper

Lets try write some simple functions to sanity check the above specifications. First, consider an unsafe vector lookup function:

```105: vec:(Data.Vector.Vector a)
-> {VV : (GHC.Types.Int) | (VV < vlen([vec])),(0 <= VV)} -> aunsafeLookup (Data.Vector.Vector a)vec {VV : (GHC.Types.Int) | (VV < vlen([vec])),(0 <= VV)}index = {VV : (Data.Vector.Vector a) | (VV = vec),(vlen([VV]) >= 0)}vec x:(Data.Vector.Vector a)
-> {VV : (GHC.Types.Int) | (VV < vlen([x])),(0 <= VV)} -> a! {VV : (GHC.Types.Int) | (VV = index),(VV < vlen([vec])),(0 <= VV)}index
```

If we run this through LiquidHaskell, it will spit back a type error for the expression `x ! i` because (happily!) it cannot prove that `index` is between `0` and the `vlen vec`. Of course, we can specify the bounds requirement in the input type

```114: {-@ unsafeLookup :: vec:Vector a
115:                  -> {v: Int | (0 <= v && v < (vlen vec))}
116:                  -> a
117:   @-}
```

then LiquidHaskell is happy to verify the lookup. Of course, now the burden of ensuring the index is valid is pushed to clients of `unsafeLookup`.

Instead, we might write a safe lookup function that performs the bounds check before looking up the vector:

```127: {-@ safeLookup :: Vector a -> Int -> Maybe a @-}
128: (Data.Vector.Vector a) -> (GHC.Types.Int) -> (Data.Maybe.Maybe a)safeLookup (Data.Vector.Vector a)x (GHC.Types.Int)i
129:   | {VV : (GHC.Types.Int) | (VV = (0  :  int))}0 x:(GHC.Types.Int)
-> y:(GHC.Types.Int)
-> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x <= y))}<= {VV : (GHC.Types.Int) | (VV = i)}i x:(GHC.Types.Bool)
-> y:(GHC.Types.Bool)
-> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> && [(? Prop([x]));
(? Prop([y]))])}&& {VV : (GHC.Types.Int) | (VV = i)}i x:(GHC.Types.Int)
-> y:(GHC.Types.Int)
-> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x < y))}< x:(Data.Vector.Vector a)
-> {VV : (GHC.Types.Int) | (VV = vlen([x])),(VV >= 0)}length {VV : (Data.Vector.Vector a) | (VV = x),(vlen([VV]) >= 0)}x = x:a
-> {VV : (Data.Maybe.Maybe a) | ((? isJust([VV])) <=> true),
(fromJust([VV]) = x)}Just ({VV : (Data.Vector.Vector a) | (VV = x),(vlen([VV]) >= 0)}x x:(Data.Vector.Vector a)
-> {VV : (GHC.Types.Int) | (VV < vlen([x])),(0 <= VV)} -> a! {VV : (GHC.Types.Int) | (VV = i)}i)
130:   | otherwise              = {VV : (Data.Maybe.Maybe {VV : a | false}) | ((? isJust([VV])) <=> false)}Nothing
```

Predicate Aliases

The type for `unsafeLookup` above is rather verbose as we have to spell out the upper and lower bounds and conjoin them. Just as we enjoy abstractions when programming, we will find it handy to have abstractions in the specification mechanism. To this end, LiquidHaskell supports predicate aliases, which are best illustrated by example

```142: {-@ predicate Btwn Lo I Hi = (Lo <= I && I < Hi) @-}
143: {-@ predicate InBounds I A = (Btwn 0 I (vlen A)) @-}
```

Now, we can simplify the type for the unsafe lookup function to

```149: {-@ unsafeLookup' :: x:Vector a -> {v:Int | (InBounds v x)} -> a @-}
150: unsafeLookup' :: Vector a -> Int -> a
151: x:(Data.Vector.Vector a)
-> {VV : (GHC.Types.Int) | (VV < vlen([x])),(0 <= VV)} -> aunsafeLookup' (Data.Vector.Vector a)x {VV : (GHC.Types.Int) | (VV < vlen([x])),(0 <= VV)}i = {VV : (Data.Vector.Vector a) | (VV = x),(vlen([VV]) >= 0)}x x:(Data.Vector.Vector a)
-> {VV : (GHC.Types.Int) | (VV < vlen([x])),(0 <= VV)} -> a! {VV : (GHC.Types.Int) | (VV = i),(VV < vlen([x])),(0 <= VV)}i
```

## Our First Recursive Function¶

OK, with the tedious preliminaries out of the way, lets write some code!

To start: a vanilla recursive function that adds up the absolute values of the elements of an integer vector.

```164: absoluteSum       :: Vector Int -> Int
165: (Data.Vector.Vector (GHC.Types.Int))
-> {VV : (GHC.Types.Int) | (0 <= VV)}absoluteSum (Data.Vector.Vector (GHC.Types.Int))vec   = x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV = (x  :  int))}if {VV : (GHC.Types.Int) | (VV = (0  :  int))}0 x:{VV : (GHC.Types.Int) | (VV >= 0),
(0 <= VV),
(VV <= n),
(VV <= vlen([vec]))}
-> y:{VV : (GHC.Types.Int) | (VV >= 0),
(0 <= VV),
(VV <= n),
(VV <= vlen([vec]))}
-> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x < y))}< {VV : (GHC.Types.Int) | (VV = n),(VV = vlen([vec])),(VV >= 0)}n then x6:{VV : (GHC.Types.Int) | (VV = 0),
(VV < n),
(VV < vlen([vec])),
(0 <= VV)}
-> x4:{VV : (GHC.Types.Int) | (VV = 0),
(VV = x6),
(VV < n),
(VV < vlen([vec])),
(0 <= VV),
(x6 <= VV)}
-> {VV : (GHC.Types.Int) | (VV >= 0),
(VV >= x6),
(VV >= x4),
(0 <= VV),
(x6 <= VV),
(x4 <= VV)}go {VV : (GHC.Types.Int) | (VV = (0  :  int))}0 {VV : (GHC.Types.Int) | (VV = (0  :  int))}0 else x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV = (x  :  int))}0
166:   where
167:     x6:{VV : (GHC.Types.Int) | (VV = 0),
(VV < n),
(VV < vlen([vec])),
(0 <= VV)}
-> x4:{VV : (GHC.Types.Int) | (VV = 0),
(VV = x6),
(VV < n),
(VV < vlen([vec])),
(0 <= VV),
(x6 <= VV)}
-> {VV : (GHC.Types.Int) | (VV >= 0),
(VV >= x6),
(VV >= x4),
(0 <= VV),
(x6 <= VV),
(x4 <= VV)}go {VV : (GHC.Types.Int) | (VV >= 0),(0 <= VV)}acc {VV : (GHC.Types.Int) | (VV >= 0),
(0 <= VV),
(VV <= n),
(VV <= vlen([vec]))}i
168:       | {VV : (GHC.Types.Int) | (VV = i),
(VV >= 0),
(0 <= VV),
(VV <= n),
(VV <= vlen([vec]))}i x:{VV : (GHC.Types.Int) | (VV >= 0),
(VV >= i),
(0 <= VV),
(VV <= n),
(VV <= vlen([vec])),
(i <= VV)}
-> y:{VV : (GHC.Types.Int) | (VV >= 0),
(VV >= i),
(0 <= VV),
(VV <= n),
(VV <= vlen([vec])),
(i <= VV)}
-> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x != y))}/= {VV : (GHC.Types.Int) | (VV = n),(VV = vlen([vec])),(VV >= 0)}n    = x6:{VV : (GHC.Types.Int) | (VV = 0),
(VV < n),
(VV < vlen([vec])),
(0 <= VV)}
-> x4:{VV : (GHC.Types.Int) | (VV = 0),
(VV = x6),
(VV < n),
(VV < vlen([vec])),
(0 <= VV),
(x6 <= VV)}
-> {VV : (GHC.Types.Int) | (VV >= 0),
(VV >= x6),
(VV >= x4),
(0 <= VV),
(x6 <= VV),
(x4 <= VV)}go ({VV : (GHC.Types.Int) | (VV = acc),(VV >= 0),(0 <= VV)}acc x:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV = (x + y))}+ n:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV >= 0),(VV >= n)}abz ({VV : (Data.Vector.Vector (GHC.Types.Int)) | (VV = vec),
(vlen([VV]) >= 0)}vec x:(Data.Vector.Vector (GHC.Types.Int))
-> {VV : (GHC.Types.Int) | (VV < vlen([x])),(0 <= VV)}
-> (GHC.Types.Int)! {VV : (GHC.Types.Int) | (VV = i),
(VV >= 0),
(0 <= VV),
(VV <= n),
(VV <= vlen([vec]))}i)) ({VV : (GHC.Types.Int) | (VV = i),
(VV >= 0),
(0 <= VV),
(VV <= n),
(VV <= vlen([vec]))}i x:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV = (x + y))}+ {VV : (GHC.Types.Int) | (VV = (1  :  int))}1)
169:       | otherwise = {VV : (GHC.Types.Int) | (VV = acc),(VV >= 0),(0 <= VV)}acc
170:     {VV : (GHC.Types.Int) | (VV = vlen([vec])),(VV >= 0)}n             = x:(Data.Vector.Vector (GHC.Types.Int))
-> {VV : (GHC.Types.Int) | (VV = vlen([x])),(VV >= 0)}length {VV : (Data.Vector.Vector (GHC.Types.Int)) | (VV = vec),
(vlen([VV]) >= 0)}vec
```

where the function `abz` is the absolute value function from before.

```176: (GHC.Num.Num a)
-> (GHC.Classes.Ord a) -> n:a -> {VV : a | (VV >= 0),(VV >= n)}abz an = {VV : (GHC.Integer.Type.Integer) | (VV = 0)}if a0 x:a
-> y:a -> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x <= y))}<= {VV : a | (VV = n)}n then {VV : a | (VV = n)}n else (a0 x:a -> y:a -> {VV : a | (VV = (x - y))}- {VV : a | (VV = n)}n)
```

## Digression: Introducing Errors¶

If you are following along in the demo page -- I heartily recommend that you try the following modifications, one at a time, and see what happens.

What happens if:

1. You remove the check `0 < n` (see `absoluteSumNT` in the demo code)

2. You replace the guard with `i <= n`

In the former case, LiquidHaskell will verify safety, but in the latter case, it will grumble that your program is unsafe.

Do you understand why? (Thanks to smog_alado for pointing this out :))

## Refinement Type Inference¶

LiquidHaskell happily verifies `absoluteSum` -- or, to be precise, the safety of the vector accesses `vec ! i`. The verification works out because LiquidHaskell is able to automatically infer a suitable type for `go`. Shuffle your mouse over the identifier above to see the inferred type. Observe that the type states that the first parameter `acc` (and the output) is `0 <= V`. That is, the returned value is non-negative.

More importantly, the type states that the second parameter `i` is `0 <= V` and `V <= n` and `V <= (vlen vec)`. That is, the parameter `i` is between `0` and the vector length (inclusive). LiquidHaskell uses these and the test that `i /= n` to establish that `i` is in fact between `0` and `(vlen vec)` thereby verifing safety.

In fact, if we want to use the function externally (i.e. in another module) we can go ahead and strengthen its type to specify that the output is non-negative.

```221: {-@ absoluteSum :: Vector Int -> {v: Int | 0 <= v}  @-}
```

What happens if: You replace the output type for `absoluteSum` with `{v: Int | 0 < v }` ?

## Bottling Recursion With a Higher-Order `loop`¶

Next, lets refactor the above low-level recursive function into a generic higher-order `loop`.

```233: loop :: Int -> Int -> a -> (Int -> a -> a) -> a
234: lo:{VV : (GHC.Types.Int) | (0 <= VV)}
-> hi:{VV : (GHC.Types.Int) | (lo <= VV)}
-> a
-> ({VV : (GHC.Types.Int) | (VV < hi),(lo <= VV)} -> a -> a)
-> aloop {VV : (GHC.Types.Int) | (0 <= VV)}lo {VV : (GHC.Types.Int) | (lo <= VV)}hi abase {VV : (GHC.Types.Int) | (VV < hi),(lo <= VV)} -> a -> af = {VV : a | (VV = base)}
-> {VV : (GHC.Types.Int) | (VV = lo),
(VV >= 0),
(0 <= VV),
(VV <= hi),
(lo <= VV)}
-> ago {VV : a | (VV = base)}base {VV : (GHC.Types.Int) | (VV = lo),(0 <= VV)}lo
235:   where
236:     {VV : a | (VV = base)}
-> {VV : (GHC.Types.Int) | (VV = lo),
(VV >= 0),
(0 <= VV),
(VV <= hi),
(lo <= VV)}
-> ago aacc {VV : (GHC.Types.Int) | (VV >= 0),
(VV >= lo),
(VV >= lo),
(0 <= VV),
(VV <= hi),
(VV <= hi),
(lo <= VV),
(lo <= VV)}i
237:       | {VV : (GHC.Types.Int) | (VV = i),
(VV >= 0),
(VV >= lo),
(VV >= lo),
(0 <= VV),
(VV <= hi),
(VV <= hi),
(lo <= VV),
(lo <= VV)}i x:{VV : (GHC.Types.Int) | (VV >= 0),
(VV >= i),
(VV >= lo),
(VV >= lo),
(0 <= VV),
(VV <= hi),
(VV <= hi),
(i <= VV),
(lo <= VV),
(lo <= VV)}
-> y:{VV : (GHC.Types.Int) | (VV >= 0),
(VV >= i),
(VV >= lo),
(VV >= lo),
(0 <= VV),
(VV <= hi),
(VV <= hi),
(i <= VV),
(lo <= VV),
(lo <= VV)}
-> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x != y))}/= {VV : (GHC.Types.Int) | (VV = hi),
(VV = hi),
(VV >= 0),
(VV >= lo),
(VV >= lo),
(0 <= VV),
(hi <= VV),
(lo <= VV),
(lo <= VV)}hi   = {VV : a | (VV = base)}
-> {VV : (GHC.Types.Int) | (VV = lo),
(VV >= 0),
(0 <= VV),
(VV <= hi),
(lo <= VV)}
-> ago ({VV : (GHC.Types.Int) | (VV >= 0),
(VV >= lo),
(VV >= lo),
(VV < hi),
(VV < hi),
(0 <= VV),
(lo <= VV),
(lo <= VV)}
-> a -> af {VV : (GHC.Types.Int) | (VV = i),
(VV >= 0),
(VV >= lo),
(VV >= lo),
(0 <= VV),
(VV <= hi),
(VV <= hi),
(lo <= VV),
(lo <= VV)}i {VV : a | (VV = acc)}acc) ({VV : (GHC.Types.Int) | (VV = i),
(VV >= 0),
(VV >= lo),
(VV >= lo),
(0 <= VV),
(VV <= hi),
(VV <= hi),
(lo <= VV),
(lo <= VV)}i x:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV = (x + y))}+ {VV : (GHC.Types.Int) | (VV = (1  :  int))}1)
238:       | otherwise = {VV : a | (VV = acc)}acc
```

Using `loop` to compute `absoluteSum`

We can now use `loop` to implement `absoluteSum` like so:

```246: (GHC.Num.Num a)
-> {VV : (Data.Vector.Vector {VV : a | false}) | false}
-> {VV : a | false}absoluteSum' {VV : (Data.Vector.Vector {VV : a | false}) | false}vec = {VV : (GHC.Integer.Type.Integer) | (VV = 0)}if {VV : (GHC.Types.Int) | (VV = (0  :  int))}0 x:{VV : (GHC.Types.Int) | false}
-> y:{VV : (GHC.Types.Int) | false}
-> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x < y))}< {VV : (GHC.Types.Int) | (VV = n),(VV = vlen([vec])),(VV >= 0)}n then lo:{VV : (GHC.Types.Int) | (0 <= VV)}
-> hi:{VV : (GHC.Types.Int) | (lo <= VV)}
-> {VV : a | false}
-> ({VV : (GHC.Types.Int) | (VV < hi),(lo <= VV)}
-> {VV : a | false} -> {VV : a | false})
-> {VV : a | false}loop {VV : (GHC.Types.Int) | (VV = (0  :  int))}0 {VV : (GHC.Types.Int) | (VV = n),(VV = vlen([vec])),(VV >= 0)}n a0 {VV : (GHC.Types.Int) | false}
-> {VV : a | false} -> {VV : a | false}body else {VV : (GHC.Integer.Type.Integer) | (VV = 0)}0
247:   where {VV : (GHC.Types.Int) | false}
-> {VV : a | false} -> {VV : a | false}body     = \{VV : (GHC.Types.Int) | false}i {VV : a | false}acc -> {VV : a | false}acc x:a -> y:a -> {VV : a | (VV = (x + y))}+ ({VV : (Data.Vector.Vector {VV : a | false}) | false}vec x:(Data.Vector.Vector {VV : a | false})
-> {VV : (GHC.Types.Int) | (VV < vlen([x])),(0 <= VV)}
-> {VV : a | false}! {VV : (GHC.Types.Int) | false}i)
248:         {VV : (GHC.Types.Int) | (VV = vlen([vec])),(VV >= 0)}n        = x:(Data.Vector.Vector {VV : a | false})
-> {VV : (GHC.Types.Int) | (VV = vlen([x])),(VV >= 0)}length {VV : (Data.Vector.Vector {VV : a | false}) | false}vec
```

LiquidHaskell verifies `absoluteSum'` without any trouble.

It is very instructive to see the type that LiquidHaskell infers for `loop` -- it looks something like

```257: {-@ loop :: lo: {v: Int | (0 <= v) }
258:          -> hi: {v: Int | (lo <= v) }
259:          -> a
260:          -> (i: {v: Int | (Btwn lo v hi)} -> a -> a)
261:          -> a
262:   @-}
```

In english, the above type states that

• `lo` the loop lower bound is a non-negative integer
• `hi` the loop upper bound is a greater than `lo`,
• `f` the loop body is only called with integers between `lo` and `hi`.

Inference is a rather convenient option -- it can be tedious to have to keep typing things like the above! Of course, if we wanted to make `loop` a public or exported function, we could use the inferred type to generate an explicit signature too.

At the call

```277: loop 0 n 0 body
```

the parameters `lo` and `hi` are instantiated with `0` and `n` respectively (which, by the way is where the inference engine deduces non-negativity from) and thus LiquidHaskell concludes that `body` is only called with values of `i` that are between `0` and `(vlen vec)`, which shows the safety of the call `vec ! i`.

Using `loop` to compute `dotProduct`

Here's another use of `loop` -- this time to compute the `dotProduct` of two vectors.

```292: dotProduct     :: Vector Int -> Vector Int -> Int
293: x:(Data.Vector.Vector (GHC.Types.Int))
-> {VV : (Data.Vector.Vector (GHC.Types.Int)) | (vlen([VV]) = vlen([x]))}
-> (GHC.Types.Int)dotProduct (Data.Vector.Vector (GHC.Types.Int))x {VV : (Data.Vector.Vector (GHC.Types.Int)) | (vlen([VV]) = vlen([x]))}y = lo:{VV : (GHC.Types.Int) | (0 <= VV)}
-> hi:{VV : (GHC.Types.Int) | (lo <= VV)}
-> (GHC.Types.Int)
-> ({VV : (GHC.Types.Int) | (VV < hi),(lo <= VV)}
-> (GHC.Types.Int) -> (GHC.Types.Int))
-> (GHC.Types.Int)loop {VV : (GHC.Types.Int) | (VV = (0  :  int))}0 (x:(Data.Vector.Vector (GHC.Types.Int))
-> {VV : (GHC.Types.Int) | (VV = vlen([x])),(VV >= 0)}length {VV : (Data.Vector.Vector (GHC.Types.Int)) | (VV = x),
(vlen([VV]) >= 0)}x) {VV : (GHC.Types.Int) | (VV = (0  :  int))}0 ({VV : (GHC.Types.Int) | (VV >= 0),
(VV < vlen([x])),
(VV < vlen([y])),
(0 <= VV)}
-> (GHC.Types.Int) -> (GHC.Types.Int)\{VV : (GHC.Types.Int) | (VV >= 0),
(VV < vlen([x])),
(VV < vlen([y])),
(0 <= VV)}i -> (x:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV = (x + y))}+ ({VV : (Data.Vector.Vector (GHC.Types.Int)) | (VV = x),
(vlen([VV]) >= 0)}x x:(Data.Vector.Vector (GHC.Types.Int))
-> {VV : (GHC.Types.Int) | (VV < vlen([x])),(0 <= VV)}
-> (GHC.Types.Int)! {VV : (GHC.Types.Int) | (VV = i),
(VV >= 0),
(VV < vlen([x])),
(VV < vlen([y])),
(0 <= VV)}i) x:(GHC.Types.Int)
-> y:(GHC.Types.Int)
-> {VV : (GHC.Types.Int) | (&& [(x >= 0); (y >= 0)] => (VV >= 0))}* ({VV : (Data.Vector.Vector (GHC.Types.Int)) | (VV = y),
(vlen([VV]) = vlen([x])),
(vlen([VV]) >= 0)}y x:(Data.Vector.Vector (GHC.Types.Int))
-> {VV : (GHC.Types.Int) | (VV < vlen([x])),(0 <= VV)}
-> (GHC.Types.Int)! {VV : (GHC.Types.Int) | (VV = i),
(VV >= 0),
(VV < vlen([x])),
(VV < vlen([y])),
(0 <= VV)}i)))
```

The gimlet-eyed reader will realize that the above is quite unsafe -- what if `x` is a 10-dimensional vector while `y` has only 3-dimensions?

A nasty

```300: *** Exception: ./Data/Vector/Generic.hs:244 ((!)): index out of bounds ...
```

Yech.

This is precisely the sort of unwelcome surprise we want to do away with at compile-time. Refinements to the rescue! We can specify that the vectors have the same dimensions quite easily

```310: {-@ dotProduct :: x:(Vector Int)
311:                -> y:{v: (Vector Int) | (vlen v) = (vlen x)}
312:                -> Int
313:   @-}
```

after which LiquidHaskell will gladly verify that the implementation of `dotProduct` is indeed safe!

## Refining Data Types¶

Next, suppose we want to write a sparse dot product, that is, the dot product of a vector and a sparse vector represented by a list of index-value tuples.

Representing Sparse Vectors

We can represent the sparse vector with a refinement type alias

```331: {-@ type SparseVector a N = [({v: Int | (Btwn 0 v N)}, a)] @-}
```

As with usual types, the alias `SparseVector` on the left is just a shorthand for the (longer) type on the right, it does not actually define a new type. Thus, the above alias is simply a refinement of Haskell's `[(Int, a)]` type, with a size parameter `N` that facilitates easy specification reuse. In this way, refinements let us express invariants of containers like lists in a straightforward manner.

Aside: If you are familiar with the index-style length encoding e.g. as found in DML or Agda, then note that despite appearances, our `SparseVector` definition is not indexed. Instead, we deliberately choose to encode properties with logical refinement predicates, to facilitate SMT based checking and inference.

Verifying Uses of Sparse Vectors

Next, we can write a recursive procedure that computes the sparse product

```353: {-@ sparseProduct :: (Num a) => x:(Vector a)
354:                              -> SparseVector a (vlen x)
355:                              -> a
356:   @-}
357: (GHC.Num.Num a)
-> x:(Data.Vector.Vector a)
-> [({VV : (GHC.Types.Int) | (VV < vlen([x])),(0 <= VV)} , a)]
-> asparseProduct (Data.Vector.Vector a)x [({VV : (GHC.Types.Int) | (VV < vlen([x])),(0 <= VV)} , a)]y  = {VV : a | (VV = 0)}
-> {VV : [({VV : (GHC.Types.Int) | (VV >= 0),
(VV < vlen([x])),
(0 <= VV)} , a)] | (VV = y),
(len([VV]) = len([y])),
(len([VV]) >= 0)}
-> ago a0 {VV : [({VV : (GHC.Types.Int) | (VV < vlen([x])),
(0 <= VV)} , a)] | (VV = y),(len([VV]) >= 0)}y
358:   where
359:     {VV : a | (VV = 0)}
-> {VV : [({VV : (GHC.Types.Int) | (VV >= 0),
(VV < vlen([x])),
(0 <= VV)} , a)] | (VV = y),
(len([VV]) = len([y])),
(len([VV]) >= 0)}
-> ago asum ((i, v) : y') = {VV : a | (VV = 0)}
-> {VV : [({VV : (GHC.Types.Int) | (VV >= 0),
(VV < vlen([x])),
(0 <= VV)} , a)] | (VV = y),
(len([VV]) = len([y])),
(len([VV]) >= 0)}
-> ago ({VV : a | (VV = sum)}sum x:a -> y:a -> {VV : a | (VV = (x + y))}+ a({VV : (Data.Vector.Vector a) | (VV = x),
(VV = x),
(vlen([VV]) = vlen([x])),
(vlen([VV]) >= 0)}x x:(Data.Vector.Vector a)
-> {VV : (GHC.Types.Int) | (VV < vlen([x])),(0 <= VV)} -> a! {VV : (GHC.Types.Int) | (VV = i),
(VV >= 0),
(VV < vlen([x])),
(VV < vlen([x])),
(0 <= VV)}i) x:a -> y:a -> {VV : a | (&& [(x >= 0); (y >= 0)] => (VV >= 0))}* {VV : a | (VV = v)}v) {VV : [({VV : (GHC.Types.Int) | (VV >= 0),
(VV < vlen([x])),
(VV < vlen([x])),
(0 <= VV)} , a)] | (VV = y'),(len([VV]) >= 0)}y'
360:     go sum []            = {VV : a | (VV = sum)}sum
```

LiquidHaskell verifies the above by using the specification for `y` to conclude that for each tuple `(i, v)` in the list, the value of `i` is within the bounds of the vector `x`, thereby proving the safety of the access `x ! i`.

## Refinements and Polymorphism¶

The sharp reader will have undoubtedly noticed that the sparse product can be more cleanly expressed as a fold.

Indeed! Let us recall the type of the `foldl` operation

```375: foldl' :: (a -> b -> a) -> a -> [b] -> a
```

Thus, we can simply fold over the sparse vector, accumulating the `sum` as we go along

```382: {-@ sparseProduct' :: (Num a) => x:(Vector a)
383:                              -> SparseVector a (vlen x)
384:                              -> a
385:   @-}
386: (GHC.Num.Num a)
-> x:(Data.Vector.Vector a)
-> [({VV : (GHC.Types.Int) | (VV < vlen([x])),(0 <= VV)} , a)]
-> asparseProduct' (Data.Vector.Vector a)x [({VV : (GHC.Types.Int) | (VV < vlen([x])),(0 <= VV)} , a)]y  = (a
-> ({VV : (GHC.Types.Int) | (VV >= 0),
(VV < vlen([x])),
(0 <= VV)} , a)
-> a)
-> a
-> [({VV : (GHC.Types.Int) | (VV >= 0),
(VV < vlen([x])),
(0 <= VV)} , a)]
-> afoldl' a
-> ({VV : (GHC.Types.Int) | (VV >= 0),
(VV < vlen([x])),
(0 <= VV)} , a)
-> abody a0 {VV : [({VV : (GHC.Types.Int) | (VV < vlen([x])),
(0 <= VV)} , a)] | (VV = y),(len([VV]) >= 0)}y
387:   where
388:     a
-> ({VV : (GHC.Types.Int) | (VV >= 0),
(VV < vlen([x])),
(0 <= VV)} , a)
-> abody asum (i, v) = {VV : a | (VV = sum)}sum x:a -> y:a -> {VV : a | (VV = (x + y))}+ a({VV : (Data.Vector.Vector a) | (VV = x),(vlen([VV]) >= 0)}x x:(Data.Vector.Vector a)
-> {VV : (GHC.Types.Int) | (VV < vlen([x])),(0 <= VV)} -> a! {VV : (GHC.Types.Int) | (VV = i),
(VV >= 0),
(VV < vlen([x])),
(0 <= VV)}i) x:a -> y:a -> {VV : a | (&& [(x >= 0); (y >= 0)] => (VV >= 0))}* {VV : a | (VV = v)}v
```

LiquidHaskell digests this too, without much difficulty.

The main trick is in how the polymorphism of `foldl'` is instantiated.

1. The GHC type inference engine deduces that at this site, the type variable `b` from the signature of `foldl'` is instantiated to the Haskell type `(Int, a)`.

2. Correspondingly, LiquidHaskell infers that in fact `b` can be instantiated to the refined type `({v: Int | (Btwn 0 v (vlen x))}, a)`.

Walk the mouse over to `i` to see this inferred type. (You can also hover over `foldl'`above to see the rather more verbose fully instantiated type.)

Thus, the inference mechanism saves us a fair bit of typing and allows us to reuse existing polymorphic functions over containers and such without ceremony.

## Conclusion¶

That's all for now folks! Hopefully the above gives you a reasonable idea of how one can use refinements to verify size related properties, and more generally, to specify and verify properties of recursive, and polymorphic functions operating over datatypes. Next time, we'll look at how we can teach LiquidHaskell to think about properties of recursive structures like lists and trees.

Ranjit Jhala
2013-03-04 16:12