Hopefully, these [articlesref102 gave you a basic idea about what basic refinement types look like. Today, lets move on to some fancier properties, 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.
23: module VectorBounds ( 24: safeLookup 25: , unsafeLookup, unsafeLookup' 26: , absoluteSum, absoluteSum' 27: , dotProduct 28: , sparseProduct, sparseProduct' 29: ) where 30: 31: import Prelude hiding (length) 32: import Data.List (foldl') 33: 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. In this article, we will illustrate this use case by writing a few short functions that manipulate vectors, in particular, those from the popular vector library.
To start off, lets specify bounds safety by refining the types for
the key functions exported by the module Data.Vector.
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
vlenwhich denotes the size of the vector, - assume that the
lengthfunction returns an integer equal to the vector’s size, and - assume that the lookup function
!requires an index between0and the vector’s size.
There are several things worth paying close attention to in the above snippet.
Measures
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.
90: 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:
104: forall a. vec:(Vector a) -> {VV : (Int) | (VV < vlen([vec])),(0 <= VV)} -> aunsafeLookup (Vector a)vec {VV : (Int) | (VV >= 0),(VV < vlen([vec])),(0 <= VV)}index = {VV : (Vector a) | (VV = vec),(vlen([VV]) >= 0)}vec x:(Vector a) -> {VV : (Int) | (VV < vlen([x])),(0 <= VV)} -> a! {VV : (Int) | (VV = index),(VV >= 0),(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
113: {-@ unsafeLookup :: vec:Vector a 114: -> {v: Int | (0 <= v && v < (vlen vec))} 115: -> a 116: @-}
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:
126: forall a. {VV : (Vector {VV : a | false}) | false} -> {VV : (Int) | false} -> {VV : (Maybe {VV : a | false}) | false}safeLookup {VV : (Vector {VV : a | false}) | false}x {VV : (Int) | false}i 127: | {VV : (Int) | (VV = (0 : int))}0 x:{VV : (Int) | false} -> y:{VV : (Int) | false} -> {VV : (Bool) | ((? Prop([VV])) <=> (x <= y))}<= {VV : (Int) | false}i x:(Bool) -> y:(Bool) -> {VV : (Bool) | ((? Prop([VV])) <=> && [(? Prop([x])); (? Prop([y]))])}&& {VV : (Int) | false}i x:{VV : (Int) | false} -> y:{VV : (Int) | false} -> {VV : (Bool) | ((? Prop([VV])) <=> (x < y))}< x:(Vector {VV : a | false}) -> {VV : (Int) | (VV = vlen([x])),(VV >= 0)}length {VV : (Vector {VV : a | false}) | false}x = x:{VV : a | false} -> {VV : (Maybe {VV : a | false}) | ((? isJust([VV])) <=> true), (fromJust([VV]) = x)}Just ({VV : (Vector {VV : a | false}) | false}x x:(Vector {VV : a | false}) -> {VV : (Int) | (VV < vlen([x])),(0 <= VV)} -> {VV : a | false}! {VV : (Int) | false}i) 128: | otherwise = {VV : (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
140: {-@ predicate Btwn Lo I Hi = (Lo <= I && I < Hi) @-} 141: {-@ predicate InBounds I A = (Btwn 0 I (vlen A)) @-}
Now, we can simplify the type for the unsafe lookup function to
147: {-@ unsafeLookup' :: x:Vector a -> {v:Int | (InBounds v x)} -> a @-} 148: unsafeLookup' :: Vector a -> Int -> a 149: forall a. x:(Vector a) -> {VV : (Int) | (VV < vlen([x])),(0 <= VV)} -> aunsafeLookup' (Vector a)x {VV : (Int) | (VV >= 0),(VV < vlen([x])),(0 <= VV)}i = {VV : (Vector a) | (VV = x),(vlen([VV]) >= 0)}x x:(Vector a) -> {VV : (Int) | (VV < vlen([x])),(0 <= VV)} -> a! {VV : (Int) | (VV = i),(VV >= 0),(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.
162: absoluteSum :: Vector Int -> Int 163: (Vector (Int)) -> {VV : (Int) | (0 <= VV)}absoluteSum (Vector (Int))vec = x:(Int#) -> {VV : (Int) | (VV = (x : int))}if {VV : (Int) | (VV = (0 : int))}0 x:{VV : (Int) | (VV >= 0),(0 <= VV),(VV <= n),(VV <= vlen([vec]))} -> y:{VV : (Int) | (VV >= 0), (0 <= VV), (VV <= n), (VV <= vlen([vec]))} -> {VV : (Bool) | ((? Prop([VV])) <=> (x < y))}< {VV : (Int) | (VV = n),(VV = vlen([vec])),(VV >= 0)}n then x6:{VV : (Int) | (VV = 0),(VV < n),(VV < vlen([vec])),(0 <= VV)} -> x4:{VV : (Int) | (VV = 0), (VV = x6), (VV < n), (VV < vlen([vec])), (0 <= VV), (x6 <= VV)} -> {VV : (Int) | (VV >= 0), (VV >= x6), (VV >= x4), (0 <= VV), (x6 <= VV), (x4 <= VV)}go {VV : (Int) | (VV = (0 : int))}0 {VV : (Int) | (VV = (0 : int))}0 else x:(Int#) -> {VV : (Int) | (VV = (x : int))}0 164: where 165: x6:{VV : (Int) | (VV = 0),(VV < n),(VV < vlen([vec])),(0 <= VV)} -> x4:{VV : (Int) | (VV = 0), (VV = x6), (VV < n), (VV < vlen([vec])), (0 <= VV), (x6 <= VV)} -> {VV : (Int) | (VV >= 0), (VV >= x6), (VV >= x4), (0 <= VV), (x6 <= VV), (x4 <= VV)}go {VV : (Int) | (VV >= 0),(0 <= VV)}acc {VV : (Int) | (VV >= 0), (0 <= VV), (VV <= n), (VV <= vlen([vec])), (VV <= vlen([vec]))}i 166: | {VV : (Int) | (VV = i), (VV >= 0), (0 <= VV), (VV <= n), (VV <= vlen([vec])), (VV <= vlen([vec]))}i x:{VV : (Int) | (VV >= 0), (VV >= i), (0 <= VV), (VV <= n), (VV <= vlen([vec])), (VV <= vlen([vec])), (i <= VV)} -> y:{VV : (Int) | (VV >= 0), (VV >= i), (0 <= VV), (VV <= n), (VV <= vlen([vec])), (VV <= vlen([vec])), (i <= VV)} -> {VV : (Bool) | ((? Prop([VV])) <=> (x != y))}/= {VV : (Int) | (VV = n),(VV = vlen([vec])),(VV >= 0)}n = x6:{VV : (Int) | (VV = 0),(VV < n),(VV < vlen([vec])),(0 <= VV)} -> x4:{VV : (Int) | (VV = 0), (VV = x6), (VV < n), (VV < vlen([vec])), (0 <= VV), (x6 <= VV)} -> {VV : (Int) | (VV >= 0), (VV >= x6), (VV >= x4), (0 <= VV), (x6 <= VV), (x4 <= VV)}go ({VV : (Int) | (VV = acc),(VV >= 0),(0 <= VV)}acc x:(Int) -> y:(Int) -> {VV : (Int) | (VV = (x + y))}+ n:(Int) -> {VV : (Int) | (VV >= 0),(VV >= n)}abz ({VV : (Vector (Int)) | (VV = vec), (VV = vec), (vlen([VV]) = vlen([vec])), (vlen([VV]) >= 0)}vec x:(Vector (Int)) -> {VV : (Int) | (VV < vlen([x])),(0 <= VV)} -> (Int)! {VV : (Int) | (VV = i), (VV >= 0), (0 <= VV), (VV <= n), (VV <= vlen([vec])), (VV <= vlen([vec]))}i)) ({VV : (Int) | (VV = i), (VV >= 0), (0 <= VV), (VV <= n), (VV <= vlen([vec])), (VV <= vlen([vec]))}i x:(Int) -> y:(Int) -> {VV : (Int) | (VV = (x + y))}+ {VV : (Int) | (VV = (1 : int))}1) 167: | otherwise = {VV : (Int) | (VV = acc),(VV >= 0),(0 <= VV)}acc 168: {VV : (Int) | (VV = vlen([vec])),(VV >= 0)}n = x:(Vector (Int)) -> {VV : (Int) | (VV = vlen([x])),(VV >= 0)}length {VV : (Vector (Int)) | (VV = vec), (VV = vec), (vlen([VV]) = vlen([vec])), (vlen([VV]) >= 0)}vec
where the function abz is the absolute value function from before.
174: forall a. (Num a) -> (Ord a) -> n:a -> {VV : a | (VV >= 0),(VV >= n)}abz an = {VV : (Integer) | (VV = 0)}if a0 x:a -> y:a -> {VV : (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:
You remove the check
0 < nYou replace the guard with
i <= n
In each case, LiquidHaskell will grumble that your program is unsafe. Do you understand why?
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 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.
215: {-@ 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.
227: loop :: Int -> Int -> a -> (Int -> a -> a) -> a 228: forall a. lo:{VV : (Int) | (0 <= VV)} -> hi:{VV : (Int) | (0 <= VV),(lo <= VV)} -> a -> ({VV : (Int) | (VV < hi),(lo <= VV)} -> a -> a) -> aloop {VV : (Int) | (VV >= 0),(0 <= VV)}lo {VV : (Int) | (VV >= 0),(VV >= lo),(0 <= VV),(lo <= VV)}hi abase {VV : (Int) | (VV >= 0),(VV >= lo),(VV < hi),(0 <= VV),(lo <= VV)} -> a -> af = {VV : a | (VV = base)} -> {VV : (Int) | (VV = lo), (VV >= 0), (0 <= VV), (VV <= hi), (lo <= VV)} -> ago {VV : a | (VV = base)}base {VV : (Int) | (VV = lo),(VV >= 0),(0 <= VV)}lo 229: where 230: {VV : a | (VV = base)} -> {VV : (Int) | (VV = lo), (VV >= 0), (0 <= VV), (VV <= hi), (lo <= VV)} -> ago aacc {VV : (Int) | (VV >= 0), (VV >= lo), (VV >= lo), (0 <= VV), (VV <= hi), (VV <= hi), (lo <= VV), (lo <= VV)}i 231: | {VV : (Int) | (VV = i), (VV >= 0), (VV >= lo), (VV >= lo), (0 <= VV), (VV <= hi), (VV <= hi), (lo <= VV), (lo <= VV)}i x:{VV : (Int) | (VV >= 0), (VV >= i), (VV >= lo), (VV >= lo), (0 <= VV), (VV <= hi), (VV <= hi), (i <= VV), (lo <= VV), (lo <= VV)} -> y:{VV : (Int) | (VV >= 0), (VV >= i), (VV >= lo), (VV >= lo), (0 <= VV), (VV <= hi), (VV <= hi), (i <= VV), (lo <= VV), (lo <= VV)} -> {VV : (Bool) | ((? Prop([VV])) <=> (x != y))}/= {VV : (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 : (Int) | (VV = lo), (VV >= 0), (0 <= VV), (VV <= hi), (lo <= VV)} -> ago ({VV : (Int) | (VV >= 0), (VV >= lo), (VV >= lo), (VV < hi), (VV < hi), (0 <= VV), (lo <= VV), (lo <= VV)} -> a -> af {VV : (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 : (Int) | (VV = i), (VV >= 0), (VV >= lo), (VV >= lo), (0 <= VV), (VV <= hi), (VV <= hi), (lo <= VV), (lo <= VV)}i x:(Int) -> y:(Int) -> {VV : (Int) | (VV = (x + y))}+ {VV : (Int) | (VV = (1 : int))}1) 232: | otherwise = {VV : a | (VV = acc)}acc
Using loop to compute absoluteSum
We can now use loop to implement absoluteSum like so:
240: forall a. (Num a) -> {VV : (Vector {VV : a | false}) | false} -> {VV : a | false}absoluteSum' {VV : (Vector {VV : a | false}) | false}vec = {VV : (Integer) | (VV = 0)}if {VV : (Int) | (VV = (0 : int))}0 x:{VV : (Int) | false} -> y:{VV : (Int) | false} -> {VV : (Bool) | ((? Prop([VV])) <=> (x < y))}< {VV : (Int) | (VV = n),(VV = vlen([vec])),(VV >= 0)}n then lo:{VV : (Int) | (0 <= VV)} -> hi:{VV : (Int) | (0 <= VV),(lo <= VV)} -> {VV : a | false} -> ({VV : (Int) | (VV < hi),(lo <= VV)} -> {VV : a | false} -> {VV : a | false}) -> {VV : a | false}loop {VV : (Int) | (VV = (0 : int))}0 {VV : (Int) | (VV = n),(VV = vlen([vec])),(VV >= 0)}n a0 {VV : (Int) | false} -> {VV : a | false} -> {VV : a | false}body else {VV : (Integer) | (VV = 0)}0 241: where {VV : (Int) | false} -> {VV : a | false} -> {VV : a | false}body = \{VV : (Int) | false}i {VV : a | false}acc -> {VV : a | false}acc x:a -> y:a -> {VV : a | (VV = (x + y))}+ ({VV : (Vector {VV : a | false}) | false}vec x:(Vector {VV : a | false}) -> {VV : (Int) | (VV < vlen([x])),(0 <= VV)} -> {VV : a | false}! {VV : (Int) | false}i) 242: {VV : (Int) | (VV = vlen([vec])),(VV >= 0)}n = x:(Vector {VV : a | false}) -> {VV : (Int) | (VV = vlen([x])),(VV >= 0)}length {VV : (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
251: {-@ loop :: lo: {v: Int | (0 <= v) } 252: -> hi: {v: Int | ((0 <= v) && (lo <= v))} 253: -> a 254: -> (i: {v: Int | (Btwn lo v hi)} -> a -> a) 255: -> a 256: @-}
In english, the above type states that
lothe loop lower bound is a non-negative integerhithe loop upper bound is a greater thanlo,fthe loop body is only called with integers betweenloandhi.
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.
271: 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.
286: dotProduct :: Vector Int -> Vector Int -> Int 287: x:(Vector (Int)) -> {VV : (Vector (Int)) | (vlen([VV]) = vlen([x]))} -> (Int)dotProduct (Vector (Int))x {VV : (Vector (Int)) | (vlen([VV]) = vlen([x])),(vlen([VV]) >= 0)}y = lo:{VV : (Int) | (0 <= VV)} -> hi:{VV : (Int) | (0 <= VV),(lo <= VV)} -> (Int) -> ({VV : (Int) | (VV < hi),(lo <= VV)} -> (Int) -> (Int)) -> (Int)loop {VV : (Int) | (VV = (0 : int))}0 (x:(Vector (Int)) -> {VV : (Int) | (VV = vlen([x])),(VV >= 0)}length {VV : (Vector (Int)) | (VV = x),(vlen([VV]) >= 0)}x) {VV : (Int) | (VV = (0 : int))}0 ({VV : (Int) | (VV >= 0), (VV < vlen([x])), (VV < vlen([y])), (0 <= VV)} -> (Int) -> (Int)\{VV : (Int) | (VV >= 0), (VV < vlen([x])), (VV < vlen([y])), (0 <= VV)}i -> (x:(Int) -> y:(Int) -> {VV : (Int) | (VV = (x + y))}+ ({VV : (Vector (Int)) | (VV = x),(vlen([VV]) >= 0)}x x:(Vector (Int)) -> {VV : (Int) | (VV < vlen([x])),(0 <= VV)} -> (Int)! {VV : (Int) | (VV = i), (VV >= 0), (VV < vlen([x])), (VV < vlen([y])), (0 <= VV)}i) x:(Int) -> y:(Int) -> {VV : (Int) | (&& [(x >= 0); (y >= 0)] => (VV >= 0))}* ({VV : (Vector (Int)) | (VV = y), (vlen([VV]) = vlen([x])), (vlen([VV]) >= 0)}y x:(Vector (Int)) -> {VV : (Int) | (VV < vlen([x])),(0 <= VV)} -> (Int)! {VV : (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?
294: *** 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
304: {-@ dotProduct :: x:(Vector Int) 305: -> y:{v: (Vector Int) | (vlen v) = (vlen x)} 306: -> Int 307: @-}
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
325: {-@ 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
347: {-@ sparseProduct :: (Num a) => x:(Vector a) 348: -> SparseVector a (vlen x) 349: -> a 350: @-} 351: forall a. (Num a) -> x:(Vector a) -> [({VV : (Int) | (VV < vlen([x])),(0 <= VV)} , a)] -> asparseProduct (Vector a)x [({VV : (Int) | (VV >= 0),(VV < vlen([x])),(0 <= VV)} , a)]y = {VV : a | (VV = 0)} -> {VV : [({VV : (Int) | (VV >= 0), (VV < vlen([x])), (0 <= VV)} , a)] | (VV = y), (len([VV]) = len([y])), (len([VV]) >= 0)} -> ago a0 {VV : [({VV : (Int) | (VV >= 0), (VV < vlen([x])), (0 <= VV)} , a)] | (VV = y),(len([VV]) >= 0)}y 352: where 353: {VV : a | (VV = 0)} -> {VV : [({VV : (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 : (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 : (Vector a) | (VV = x), (VV = x), (vlen([VV]) = vlen([x])), (vlen([VV]) >= 0)}x x:(Vector a) -> {VV : (Int) | (VV < vlen([x])),(0 <= VV)} -> a! {VV : (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 : (Int) | (VV >= 0), (VV < vlen([x])), (VV < vlen([x])), (0 <= VV)} , a)] | (VV = y'),(len([VV]) >= 0)}y' 354: 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 thefoldl operation
369: foldl' :: (a -> b -> a) -> a -> [b] -> a
Thus, we can simply fold over the sparse vector, accumulating the sum
as we go along
376: {-@ sparseProduct' :: (Num a) => x:(Vector a) 377: -> SparseVector a (vlen x) 378: -> a 379: @-} 380: forall a. (Num a) -> x:(Vector a) -> [({VV : (Int) | (VV < vlen([x])),(0 <= VV)} , a)] -> asparseProduct' (Vector a)x [({VV : (Int) | (VV >= 0),(VV < vlen([x])),(0 <= VV)} , a)]y = (a -> ({VV : (Int) | (VV >= 0),(VV < vlen([x])),(0 <= VV)} , a) -> a) -> a -> [({VV : (Int) | (VV >= 0),(VV < vlen([x])),(0 <= VV)} , a)] -> afoldl' a -> ({VV : (Int) | (VV >= 0),(VV < vlen([x])),(0 <= VV)} , a) -> abody a0 {VV : [({VV : (Int) | (VV >= 0), (VV < vlen([x])), (0 <= VV)} , a)] | (VV = y),(len([VV]) >= 0)}y 381: where a -> ({VV : (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 : (Vector a) | (VV = x),(vlen([VV]) >= 0)}x x:(Vector a) -> {VV : (Int) | (VV < vlen([x])),(0 <= VV)} -> a! {VV : (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.
The GHC type inference engine deduces that at this site, the type variable
bfrom the signature offoldl'is instantiated to the Haskell type(Int, a).Correspondingly, LiquidHaskell infers that in fact
bcan 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
Thats 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.