Hello again! Since we last met, much has happened that we’re rather excited about, and which we promise to get to in the fullness of time.

Today, however, lets continue with our exploration of abstract refinements. We’ll see that this rather innocent looking mechanism packs quite a punch, by showing how it can encode various ordering properties of recursive data structures.

26: module PuttingThingsInOrder where
27: 
28: import Prelude hiding (break)
29: 
30: -- Haskell Type Definitions
31: plusOnes                         :: [(Int, Int)]
32: insertSort, mergeSort, quickSort :: (Ord a) => [a] -> [a]

Abstract Refinements

Recall that abstract refinements are a mechanism that let us write and check types of the form

36: maxInt :: forall <p :: Int -> Prop>. Int<p> -> Int<p> -> Int<p>

which states that the output of maxInt preserves whatever invariants held for its two inputs as long as both those inputs also satisfied those invariants.

First, lets see how we can (and why we may want to) abstractly refine data types.

Polymorphic Association Lists

Suppose, we require a type for association lists. Lets define one that is polymorphic over keys k and values v

55: data AssocP k v = KVP [(k, v)]

Now, in a program, you might have multiple association lists, whose keys satisfy different properties. For example, we might have a table for mapping digits to the corresponding English string

64: digitsP :: AssocP Int String
65: (PuttingThingsInOrder.AssocP {VV : (GHC.Types.Int) | (0 <= VV) && (VV <= 9)} [(GHC.Types.Char)])digitsP = [({VV : (GHC.Types.Int) | (VV > 0) && (0 <= VV) && (VV <= 9)}, {VV : [(GHC.Types.Char)] | ((len VV) >= 0)})]
-> (PuttingThingsInOrder.AssocP {VV : (GHC.Types.Int) | (VV > 0) && (0 <= VV) && (VV <= 9)} {VV : [(GHC.Types.Char)] | ((len VV) >= 0)})KVP [ ({VV : (GHC.Types.Int) | (VV == 1) && (VV > 0)}, {VV : [(GHC.Types.Char)] | ((len VV) >= 0)})<\_ VV -> ((len VV) >= 0)>({VV : (GHC.Types.Int) | (VV == (1  :  int))}1, {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"one")
66:               , ({VV : (GHC.Types.Int) | (VV > 0) && (0 <= VV) && (VV <= 9)}, {VV : [(GHC.Types.Char)] | ((len VV) >= 0)})<\_ VV -> ((len VV) >= 0)>({VV : (GHC.Types.Int) | (VV == (2  :  int))}2, {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"two")
67:               , ({VV : (GHC.Types.Int) | (VV > 0) && (0 <= VV) && (VV <= 9)}, {VV : [(GHC.Types.Char)] | ((len VV) >= 0)})<\_ VV -> ((len VV) >= 0)>({VV : (GHC.Types.Int) | (VV == (3  :  int))}3, {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"three") ]

We could have a separate table for sparsely storing the contents of an array of size 1000.

74: sparseVecP :: AssocP Int Double
75: (PuttingThingsInOrder.AssocP {VV : (GHC.Types.Int) | (0 <= VV) && (VV <= 1000)} (GHC.Types.Double))sparseVecP = [({VV : (GHC.Types.Int) | (VV > 0) && (0 <= VV) && (VV <= 1000)}, (GHC.Types.Double))]
-> (PuttingThingsInOrder.AssocP {VV : (GHC.Types.Int) | (VV > 0) && (0 <= VV) && (VV <= 1000)} (GHC.Types.Double))KVP [ ({VV : (GHC.Types.Int) | (VV > 0) && (0 <= VV) && (VV <= 1000)}, (GHC.Types.Double))({VV : (GHC.Types.Int) | (VV == (12  :  int))}12 ,  (GHC.Types.Double)34.1 )
76:                  , ({VV : (GHC.Types.Int) | (VV > 0) && (0 <= VV) && (VV <= 1000)}, (GHC.Types.Double))({VV : (GHC.Types.Int) | (VV == (92  :  int))}92 , (GHC.Types.Double)902.83)
77:                  , ({VV : (GHC.Types.Int) | (VV > 0) && (0 <= VV) && (VV <= 1000)}, (GHC.Types.Double))({VV : (GHC.Types.Int) | (VV == (451  :  int))}451,   (GHC.Types.Double)2.95)
78:                  , ({VV : (GHC.Types.Int) | (VV > 0) && (0 <= VV) && (VV <= 1000)}, (GHC.Types.Double))({VV : (GHC.Types.Int) | (VV == (877  :  int))}877,   (GHC.Types.Double)3.1 )]

The keys used in the two tables have rather different properties, which we may want to track at compile time.

• In digitsP the keys are between 0 and 9
• In sparseVecP the keys are between 0 and 999.

Well, since we had the foresight to parameterize the key type in AssocP, we can express the above properties by appropriately instantiating the type of k with refined versions

94: {-@ digitsP :: AssocP {v:Int | (Btwn 0 v 9)} String @-}

and

100: {-@ sparseVecP :: AssocP {v:Int | (Btwn 0 v 1000)} Double @-}

where Btwn is just an alias

106: {-@ predicate Btwn Lo V Hi = (Lo <= V && V <= Hi) @-}

Monomorphic Association Lists

Now, suppose that for one reason or another, we want to specialize our association list so that the keys are of type Int.

117: data Assoc v = KV [(Int, v)]

(We’d probably also want to exploit the Int-ness in the implementation but thats a tale for another day.)

Now, we have our two tables

126: digits    :: Assoc String
127: (PuttingThingsInOrder.Assoc [(GHC.Types.Char)])digits    = forall <p :: (GHC.Types.Int)-> Bool>.
[({VV : (GHC.Types.Int)<p> | true}, {VV : [(GHC.Types.Char)] | ((len VV) >= 0)})]
-> (PuttingThingsInOrder.Assoc <p> {VV : [(GHC.Types.Char)] | ((len VV) >= 0)})KV [ ({VV : (GHC.Types.Int) | (VV == 1) && (VV > 0)}, {VV : [(GHC.Types.Char)] | ((len VV) >= 0)})<\_ VV -> ((len VV) >= 0)>({VV : (GHC.Types.Int) | (VV == (1  :  int))}1, {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"one")
128:                , ({VV : (GHC.Types.Int) | (VV > 0) && (0 <= VV) && (VV <= 9)}, {VV : [(GHC.Types.Char)] | ((len VV) >= 0)})<\_ VV -> ((len VV) >= 0)>({VV : (GHC.Types.Int) | (VV == (2  :  int))}2, {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"two")
129:                , ({VV : (GHC.Types.Int) | (VV > 0) && (0 <= VV) && (VV <= 9)}, {VV : [(GHC.Types.Char)] | ((len VV) >= 0)})<\_ VV -> ((len VV) >= 0)>({VV : (GHC.Types.Int) | (VV == (3  :  int))}3, {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"three") ]
130: 
131: sparseVec :: Assoc Double
132: (PuttingThingsInOrder.Assoc (GHC.Types.Double))sparseVec = forall <p :: (GHC.Types.Int)-> Bool>.
[({VV : (GHC.Types.Int)<p> | true}, (GHC.Types.Double))]
-> (PuttingThingsInOrder.Assoc <p> (GHC.Types.Double))KV [ ({VV : (GHC.Types.Int) | (VV > 0) && (0 <= VV) && (VV <= 1000)}, (GHC.Types.Double))({VV : (GHC.Types.Int) | (VV == (12  :  int))}12 ,  (GHC.Types.Double)34.1 )
133:                , ({VV : (GHC.Types.Int) | (VV > 0) && (0 <= VV) && (VV <= 1000)}, (GHC.Types.Double))({VV : (GHC.Types.Int) | (VV == (92  :  int))}92 , (GHC.Types.Double)902.83)
134:                , ({VV : (GHC.Types.Int) | (VV > 0) && (0 <= VV) && (VV <= 1000)}, (GHC.Types.Double))({VV : (GHC.Types.Int) | (VV == (451  :  int))}451,   (GHC.Types.Double)2.95)
135:                , ({VV : (GHC.Types.Int) | (VV > 0) && (0 <= VV) && (VV <= 1000)}, (GHC.Types.Double))({VV : (GHC.Types.Int) | (VV == (877  :  int))}877,   (GHC.Types.Double)3.1 )]

but since we didn’t make the key type generic, it seems we have no way to distinguish between the invariants of the two sets of keys. Bummer!

Abstractly Refined Data

We could define two separate types of association lists that capture different invariants, but frankly, thats rather unfortunate, as we’d then have to duplicate the code the manipulates the structures. Of course, we’d like to have (type) systems help keep an eye on different invariants, but we’d really rather not have to duplicate code to achieve that end. Thats the sort of thing that drives a person to JavaScript ;-).

Fortunately, all is not lost.

If you were paying attention last time then you’d realize that this is the perfect job for an abstract refinement, this time applied to a data definition:

163: {-@ data Assoc v <p :: Int -> Prop> 
164:       = KV (z :: [(Int<p>, v)]) @-} 

The definition refines the type for Assoc to introduce an abstract refinement p which is, informally speaking, a property of Int. The definition states that each Int in the association list in fact satisfies p as, Int<p> is an abbreviation for {v:Int| (p v)}.

Now, we can have our Int keys and refine them too! For example, we can write:

177: {-@ digits :: Assoc (String) <{\v -> (Btwn 0 v 9)}> @-}

to track the invariant for the digits map, and write

183: {-@ sparseVec :: Assoc Double <{\v -> (Btwn 0 v 1000)}> @-}

Thus, we can recover (some of) the benefits of abstracting over the type of the key by instead parameterizing the type directly over the possible invariants. We will have much more to say on association lists (or more generally, finite maps) and abstract refinements, but lets move on for the moment.

Dependent Tuples

It is no accident that we have reused Haskell’s function type syntax to define abstract refinements (p :: Int -> Prop); interesting things start to happen if we use multiple parameters.

Consider the function break from the Prelude.

203: break                   :: (a -> Bool) -> [a] -> ([a], [a])
204: forall a.
(a -> (GHC.Types.Bool))
-> x:[a] -> ([a], [a])<\y VV -> ((len x) == ((len y) + (len VV)))>break _ [a]xs@[]           =  forall a b <p2 :: a-> b-> Bool>.
a:a
-> b:{VV : b<p2 a> | true}
-> {VV : (a, b)<p2> | ((fst VV) == a) && ((snd VV) == b)}({VV : [a] | (((null VV)) <=> true) && (VV == xs) && (VV == (GHC.Types.[])) && ((len VV) == 0) && ((len VV) >= 0)}xs, {VV : [a] | (((null VV)) <=> true) && (VV == xs) && (VV == (GHC.Types.[])) && ((len VV) == 0) && ((len VV) >= 0)}xs)
205: break p xs@(x:xs')
206:            | a -> (GHC.Types.Bool)p {VV : a | (VV == x)}x        =  forall a b <p2 :: a-> b-> Bool>.
a:a
-> b:{VV : b<p2 a> | true}
-> {VV : (a, b)<p2> | ((fst VV) == a) && ((snd VV) == b)}({VV : [{VV : a | false}]<\_ VV -> false> | (((null VV)) <=> true) && ((len VV) == 0) && ((len VV) >= 0)}[], {VV : [a] | (VV == xs) && ((len VV) >= 0)}xs)
207:            | otherwise  =  let ({VV : [a] | (VV == ys) && ((len VV) == (len ys)) && ((len xs') == ((len zs) + (len VV))) && (VV /= xs) && ((len VV) >= 0) && ((len VV) < (len xs)) && ((len VV) <= (len xs'))}ys, {VV : [a] | (VV == zs) && ((len VV) == (len zs)) && ((len xs') == ((len ys) + (len VV))) && ((len xs') == ((len ys) + (len VV))) && (VV /= xs) && ((len VV) >= 0) && ((len VV) < (len xs)) && ((len VV) <= (len xs'))}zs) = (a -> (GHC.Types.Bool))
-> x:[a] -> ([a], [a])<\y VV -> ((len x) == ((len y) + (len VV)))>break a -> (GHC.Types.Bool)p {VV : [a] | (VV == xs') && ((len VV) >= 0)}xs' 
208:                            in forall a b <p2 :: a-> b-> Bool>.
a:a
-> b:{VV : b<p2 a> | true}
-> {VV : (a, b)<p2> | ((fst VV) == a) && ((snd VV) == b)}({VV : a | (VV == x)}xforall <p :: a-> a-> Bool>.
x:a
-> xs:[{VV : a<p x> | true}]<p>
-> {VV : [a]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len xs)))}:{VV : [a] | (VV == ys) && (VV == ys) && ((len VV) == (len ys)) && ((len xs') == ((len zs) + (len VV))) && (VV /= xs) && ((len VV) >= 0) && ((len VV) < (len xs)) && ((len VV) <= (len xs'))}ys,{VV : [a] | (VV == zs) && (VV == zs) && ((len VV) == (len zs)) && ((len xs') == ((len ys) + (len VV))) && ((len xs') == ((len ys) + (len VV))) && (VV /= xs) && ((len VV) >= 0) && ((len VV) < (len xs)) && ((len VV) <= (len xs'))}zs)

From the comments in Data.List, break p xs: “returns a tuple where the first element is longest prefix (possibly empty) xs of elements that do not satisfy p and second element is the remainder of the list.”

We could formalize the notion of the second-element-being-the-remainder using sizes. That is, we’d like to specify that the length of the second element equals the length of xs minus the length of the first element.
That is, we need a way to allow the refinement of the second element to depend on the value in the first refinement. Again, we could define a special kind of tuple-of-lists-type that has the above property baked in, but thats just not how we roll.

Instead, lets use abstract refinements to give us dependent tuples

225: data (a,b)<p :: a -> b -> Prop> = (x:a, b<p x>) 

Here, the abstract refinement takes two parameters, an a and a b. In the body of the tuple, the first element is named x and we specify that the second element satisfies the refinement p x, i.e. a partial application of p with the first element. In other words, the second element is a value of type {v:b | (p x v)}.

As before, we can instantiate the p in different ways. For example the whimsical

240: {-@ plusOnes :: [(Int, Int)<{\x1 x2 -> x2 = x1 + 1}>] @-}
241: [((GHC.Types.Int), (GHC.Types.Int))<\x1 VV -> (VV == (x1 + 1))>]plusOnes = {VV : [({VV : (GHC.Types.Int) | (VV > 0) && (0 <= VV) && (VV <= 1000)}, {VV : (GHC.Types.Int) | (VV > 0) && (0 <= VV) && (VV <= 1000)})<\x3 VV -> (VV == (x3 + 1)) && (VV > 0) && (VV > x3) && (0 <= VV) && (VV <= 1000)>]<\x1 VV -> (VV /= x1)> | (((null VV)) <=> false) && ((len VV) >= 0)}[({VV : (GHC.Types.Int) | (VV == 0) && (0 <= VV) && (VV <= 9)}, {VV : (GHC.Types.Int) | (VV == 1) && (VV > 0)})<\x2 VV -> (VV == 1) && (VV == (x2 + 1)) && (VV > 0) && (VV > x2)>({VV : (GHC.Types.Int) | (VV == (0  :  int))}0,{VV : (GHC.Types.Int) | (VV == (1  :  int))}1), ({VV : (GHC.Types.Int) | (VV > 0) && (0 <= VV) && (VV <= 9)}, {VV : (GHC.Types.Int) | (VV > 0) && (0 <= VV) && (VV <= 9)})<\x2 VV -> (VV == (x2 + 1)) && (VV > 0) && (VV > x2) && (0 <= VV) && (VV <= 9)>({VV : (GHC.Types.Int) | (VV == (5  :  int))}5,{VV : (GHC.Types.Int) | (VV == (6  :  int))}6), ({VV : (GHC.Types.Int) | (VV > 0) && (0 <= VV) && (VV <= 1000)}, {VV : (GHC.Types.Int) | (VV > 0) && (0 <= VV) && (VV <= 1000)})<\x2 VV -> (VV == (x2 + 1)) && (VV > 0) && (VV > x2) && (0 <= VV) && (VV <= 1000)>({VV : (GHC.Types.Int) | (VV == (999  :  int))}999,{VV : (GHC.Types.Int) | (VV == (1000  :  int))}1000)]

and returning to the remainder property for break

247: {-@ break :: (a -> Bool) -> x:[a] 
248:           -> ([a], [a])<{\y z -> (Break x y z)}> @-}

using the predicate alias

254: {-@ predicate Break X Y Z   = (len X) = (len Y) + (len Z) @-}

Abstractly Refined Lists

Right, we’ve been going on for a bit. Time to put things in order.

To recap: we’ve already seen one way to abstractly refine lists: to recover a generic means of refining a monomorphic list (e.g. the list of Int keys.) However, in that case we were talking about individual keys. Next, we build upon the dependent-tuples technique we just saw to use abstract refinements to relate different elements inside containers.

In particular, we can use them to specify that every pair of elements inside the list is related according to some abstract relation p. By instantiating p appropriately, we will be able to recover various forms of (dis) order.

Consider the refined definition of good old Haskell lists:

277: data [a] <p :: a -> a -> Prop> where
278:   | []  :: [a] <p>
279:   | (:) :: h:a -> [a<p h>]<p> -> [a]<p>

Whoa! Thats a bit of a mouthful. Lets break it down.

• The type is parameterized with a refinement p :: a -> a -> Prop Think of p as a binary relation over the a values comprising the list.

• The empty list [] is a []<p>. Clearly, the empty list has no elements whatsoever and so every pair is trivially, or rather, vacuously related by p.

• The cons constructor (:) takes a head h of type a and a tail of a<p h> values, each of which is related to h and which (recursively) are pairwise related [...]<p> and returns a list where all elements are pairwise related [a]<p>.

Pairwise Related

Note that we’re being a bit sloppy when we say pairwise related.

What we really mean is that if a list

303: [x1,...,xn] :: [a]<p>

then for each 1 <= i < j <= n we have (p xi xj).

To see why, consider the list

309: [x1, x2, x3, ...] :: [a]<p>

This list unfolds into a head and tail

313: x1                :: a
314: [x2, x3,...]      :: [a<p x1>]<p>

The above tail unfolds into

318: x2                :: a<p x1>
319: [x3, ...]         :: [a<p x1 && p x2>]<p>

And finally into

323: x3                :: a<p x1 && p x2>
324: [...]             :: [a<p x1 && p x2 && p x3>]<p>

That is, each element xj satisfies the refinement (p xi xj) for each i < j.

Using Abstractly Refined Lists

Urgh. Math is hard!

Lets see how we can program with these funnily refined lists.

For starters, we can define a few helpful type aliases.

340: {-@ type IncrList a = [a]<{\xi xj -> xi <= xj}> @-}      
341: {-@ type DecrList a = [a]<{\xi xj -> xi >= xj}> @-}
342: {-@ type UniqList a = [a]<{\xi xj -> xi /= xj}> @-}

As you might expect, an IncrList is a list of values in increasing order:

348: {-@ whatGosUp :: IncrList Integer @-}
349: [(GHC.Integer.Type.Integer)]<\xi VV -> (xi <= VV)>whatGosUp = {VV : [{VV : (GHC.Integer.Type.Integer) | (VV > 0) && (0 <= VV) && (VV <= 9)}]<\x2 VV -> (VV == (x2 + 1)) && (VV > 0) && (VV > x2) && (0 <= VV) && (VV <= 9)> | (((null VV)) <=> false) && ((len VV) >= 0)}[1,2,3]

Similarly, a DecrList contains its values in decreasing order:

355: {-@ mustGoDown :: DecrList Integer @-}
356: [(GHC.Integer.Type.Integer)]<\xi VV -> (xi >= VV)>mustGoDown = {VV : [{VV : (GHC.Integer.Type.Integer) | (VV > 0) && (0 <= VV) && (VV <= 9)}]<\x3 VV -> (VV == 1) && (x3 /= VV) && (VV > 0) && (x3 >= VV) && (VV < x3)> | (((null VV)) <=> false) && ((len VV) >= 0)}[3,2,1]

My personal favorite though, is a UniqList which has no duplicates:

362: {-@ noDuplicates :: UniqList Integer @-}
363: [(GHC.Integer.Type.Integer)]<\xi VV -> (xi /= VV)>noDuplicates = {VV : [{VV : (GHC.Integer.Type.Integer) | (VV > 0) && (0 <= VV) && (VV <= 9)}]<\x3 VV -> (x3 /= VV) && (VV > 0) && (x3 >= VV) && (VV < x3) && (0 <= VV) && (VV <= 9)> | (((null VV)) <=> false) && ((len VV) >= 0)}[1,3,2]

Sorting Lists

Its all very well to specify lists with various kinds of invariants. The question is, how easy is it to establish these invariants?

Lets find out, by turning inevitably to that staple of all forms of formal verification: your usual textbook sorting procedures.

Insertion Sort

First up: insertion sort. Well, no surprises here:

380: {-@ insertSort    :: (Ord a) => xs:[a] -> (IncrList a) @-}
381: forall a. (GHC.Classes.Ord a) => [a] -> [a]<\xi VV -> (xi <= VV)>insertSort []     = forall <p :: a-> a-> Bool>.
{VV : [{VV : a | false}]<p> | (((null VV)) <=> true) && ((len VV) == 0)}[]
382: insertSort (x:xs) = a -> [a]<\xi VV -> (xi <= VV)> -> [a]<\xi VV -> (xi <= VV)>insert {VV : a | (VV == x)}x ([a] -> [a]<\xi VV -> (xi <= VV)>insertSort {VV : [a] | (VV == xs) && ((len VV) >= 0)}xs) 

The hard work is done by insert which places an element into the correct position of a sorted list

389: forall a.
(GHC.Classes.Ord a) =>
a
-> x1:[a]<\x2 VV -> (VV >= x2)>
-> {VV : [a]<\x1 VV -> (VV >= x1)> | (VV /= x1) && ((len VV) > 0) && ((len VV) > (len x1))}insert ay []     = {VV : [{VV : a | false}]<\_ VV -> false> | (((null VV)) <=> true) && ((len VV) == 0) && ((len VV) >= 0)}[{VV : a | (VV == y)}y]
390: insert y (x:xs) 
391:   | {VV : a | (VV == y)}y x:a -> y:a -> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x <= y))}<= {VV : a | (VV == x)}x      = {VV : a | (VV == y)}y forall <p :: a-> a-> Bool>.
x:{VV : a | (VV >= y)}
-> xs:[{VV : a<p x> | (VV >= y)}]<p>
-> {VV : [{VV : a | (VV >= y)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len xs)))}: {VV : a | (VV == x)}x forall <p :: a-> a-> Bool>.
x:{VV : a | (VV >= x) && (VV >= y)}
-> xs:[{VV : a<p x> | (VV >= x) && (VV >= y)}]<p>
-> {VV : [{VV : a | (VV >= x) && (VV >= y)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len xs)))}: {VV : [{VV : a | (VV >= x)}]<\x1 VV -> (VV >= x1)> | (VV == xs) && ((len VV) >= 0)}xs 
392:   | otherwise   = {VV : a | (VV == x)}x forall <p :: a-> a-> Bool>.
x:{VV : a | (VV >= x)}
-> xs:[{VV : a<p x> | (VV >= x)}]<p>
-> {VV : [{VV : a | (VV >= x)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len xs)))}: forall a.
(GHC.Classes.Ord a) =>
a
-> x1:[a]<\x2 VV -> (VV >= x2)>
-> {VV : [a]<\x1 VV -> (VV >= x1)> | (VV /= x1) && ((len VV) > 0) && ((len VV) > (len x1))}insert {VV : a | (VV == y)}y {VV : [{VV : a | (VV >= x)}]<\x1 VV -> (VV >= x1)> | (VV == xs) && ((len VV) >= 0)}xs

LiquidHaskell infers that if you give insert an element and a sorted list, it returns a sorted list.

399: {-@ insert :: (Ord a) => a -> IncrList a -> IncrList a @-}

If you prefer the more Haskelly way of writing insertion sort, i.e. with a foldr, that works too. Can you figure out why?

406: {-@ insertSort' :: (Ord a) => [a] -> IncrList a @-}
407: forall a. (GHC.Classes.Ord a) => [a] -> [a]<\xi VV -> (xi <= VV)>insertSort' [a]xs  = (a -> [a]<\x4 VV -> (VV >= x4)> -> [a]<\x4 VV -> (VV >= x4)>)
-> [a]<\x4 VV -> (VV >= x4)> -> [a] -> [a]<\x4 VV -> (VV >= x4)>foldr a -> [a]<\xi VV -> (xi <= VV)> -> [a]<\xi VV -> (xi <= VV)>insert {VV : [{VV : a | false}]<\_ VV -> false> | (((null VV)) <=> true) && ((len VV) == 0) && ((len VV) >= 0)}[] {VV : [a] | (VV == xs) && ((len VV) >= 0)}xs

Merge Sort

Well, you know the song goes. First, we write a function that splits the input into two parts:

416: split          :: [a] -> ([a], [a])
417: forall a.
x1:{VV : [a] | ((len VV) >= 0)}
-> ({VV : [a] | ((len VV) >= 0) && ((len VV) <= (len x1))}, {VV : [a] | ((len VV) >= 0) && ((len VV) <= (len x1))})<\x2 VV -> ((len x1) == ((len x2) + (len VV))) && ((len VV) >= 0) && ((len VV) <= (len x1)) && ((len VV) <= (len x2))>split (x:y:zs) = forall a b <p2 :: a-> b-> Bool>.
a:a
-> b:{VV : b<p2 a> | true}
-> {VV : (a, b)<p2> | ((fst VV) == a) && ((snd VV) == b)}({VV : a | (VV == x)}xforall <p :: a-> a-> Bool>.
x:a
-> xs:[{VV : a<p x> | true}]<p>
-> {VV : [a]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len xs)))}:{VV : [a] | (VV == xs) && (VV == xs) && ((len VV) == (len xs)) && ((len zs) == ((len ys) + (len VV))) && ((len VV) >= 0) && ((len VV) >= (len ys)) && ((len VV) <= (len zs))}xs, {VV : a | (VV == y)}yforall <p :: a-> a-> Bool>.
x:a
-> xs:[{VV : a<p x> | true}]<p>
-> {VV : [a]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len xs)))}:{VV : [a] | (VV == ys) && (VV == ys) && ((len VV) == (len ys)) && ((len zs) == ((len xs) + (len VV))) && ((len zs) == ((len xs) + (len VV))) && ((len VV) >= 0) && ((len VV) <= (len xs)) && ((len VV) <= (len xs)) && ((len VV) <= (len zs))}ys) 
418:   where 
419:     ({VV : [a] | (VV == xs) && ((len VV) == (len xs)) && ((len zs) == ((len ys) + (len VV))) && ((len VV) >= 0) && ((len VV) >= (len ys)) && ((len VV) <= (len zs))}xs, {VV : [a] | (VV == ys) && ((len VV) == (len ys)) && ((len zs) == ((len xs) + (len VV))) && ((len zs) == ((len xs) + (len VV))) && ((len VV) >= 0) && ((len VV) <= (len xs)) && ((len VV) <= (len xs)) && ((len VV) <= (len zs))}ys)   = forall a.
x1:{VV : [a] | ((len VV) >= 0)}
-> ({VV : [a] | ((len VV) >= 0) && ((len VV) <= (len x1))}, {VV : [a] | ((len VV) >= 0) && ((len VV) <= (len x1))})<\x2 VV -> ((len x1) == ((len x2) + (len VV))) && ((len VV) >= 0) && ((len VV) <= (len x1)) && ((len VV) <= (len x2))>split {VV : [a] | (VV == zs) && ((len VV) >= 0)}zs
420: split xs       = forall a b <p2 :: a-> b-> Bool>.
a:a
-> b:{VV : b<p2 a> | true}
-> {VV : (a, b)<p2> | ((fst VV) == a) && ((snd VV) == b)}({VV : [a] | ((len VV) >= 0)}xs, {VV : [{VV : a | false}]<\_ VV -> false> | (((null VV)) <=> true) && ((len VV) == 0) && ((len VV) >= 0)}[])

Then we need a function that merges two (sorted) lists

426: forall a.
(GHC.Classes.Ord a) =>
xs:[a]<\x3 VV -> (x3 <= VV)>
-> x1:[a]<\x2 VV -> (x2 <= VV)>
-> {VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0) && ((len VV) >= (len x1)) && ((len VV) >= (len xs))}merge [a]<\x1 VV -> (x1 <= VV)>xs []         = {VV : [a]<\x1 VV -> (x1 <= VV)> | (VV == xs) && ((len VV) >= 0)}xs
427: merge [] ys         = {VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}ys
428: merge (x:xs) (y:ys) 
429:   | {VV : a | (VV == x)}x x:a -> y:a -> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x <= y))}<= {VV : a | (VV == y)}y          = {VV : a | (VV == x)}x forall <p :: a-> a-> Bool>.
x:{VV : a | (VV >= x)}
-> xs:[{VV : a<p x> | (VV >= x)}]<p>
-> {VV : [{VV : a | (VV >= x)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len xs)))}: forall a.
(GHC.Classes.Ord a) =>
xs:[a]<\x3 VV -> (x3 <= VV)>
-> x1:[a]<\x2 VV -> (x2 <= VV)>
-> {VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0) && ((len VV) >= (len x1)) && ((len VV) >= (len xs))}merge {VV : [{VV : a | (x <= VV)}]<\x1 VV -> (x1 <= VV)> | (VV == xs) && ((len VV) >= 0)}xs ({VV : a | (VV == y)}yforall <p :: a-> a-> Bool>.
x:{VV : a | (VV >= x) && (VV >= y)}
-> xs:[{VV : a<p x> | (VV >= x) && (VV >= y)}]<p>
-> {VV : [{VV : a | (VV >= x) && (VV >= y)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len xs)))}:{VV : [{VV : a | (y <= VV)}]<\x1 VV -> (x1 <= VV)> | (VV == ys) && ((len VV) >= 0)}ys)
430:   | otherwise       = {VV : a | (VV == y)}y forall <p :: a-> a-> Bool>.
x:{VV : a | (VV >= y)}
-> xs:[{VV : a<p x> | (VV >= y)}]<p>
-> {VV : [{VV : a | (VV >= y)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len xs)))}: forall a.
(GHC.Classes.Ord a) =>
xs:[a]<\x3 VV -> (x3 <= VV)>
-> x1:[a]<\x2 VV -> (x2 <= VV)>
-> {VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0) && ((len VV) >= (len x1)) && ((len VV) >= (len xs))}merge ({VV : a | (VV == x)}xforall <p :: a-> a-> Bool>.
x:{VV : a | (VV > y) && (VV >= x)}
-> xs:[{VV : a<p x> | (VV > y) && (VV >= x)}]<p>
-> {VV : [{VV : a | (VV > y) && (VV >= x)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len xs)))}:{VV : [{VV : a | (x <= VV)}]<\x1 VV -> (x1 <= VV)> | (VV == xs) && ((len VV) >= 0)}xs) {VV : [{VV : a | (y <= VV)}]<\x1 VV -> (x1 <= VV)> | (VV == ys) && ((len VV) >= 0)}ys

LiquidHaskell deduces that if both inputs are ordered, then so is the output.

437: {-@ merge :: (Ord a) => IncrList a 
438:                      -> IncrList a 
439:                      -> IncrList a 
440:   @-}

Finally, using the above functions we write mergeSort:

446: {-@ mergeSort :: (Ord a) => [a] -> IncrList a @-}
447: forall a. (GHC.Classes.Ord a) => [a] -> [a]<\xi VV -> (xi <= VV)>mergeSort []  = forall <p :: a-> a-> Bool>.
{VV : [{VV : a | false}]<p> | (((null VV)) <=> true) && ((len VV) == 0)}[]
448: mergeSort [x] = {VV : [{VV : a | false}]<\_ VV -> false> | (((null VV)) <=> true) && ((len VV) == 0) && ((len VV) >= 0)}[{VV : a | (VV == x)}x]
449: mergeSort xs  = [a]<\xi VV -> (xi <= VV)>
-> [a]<\xi VV -> (xi <= VV)> -> [a]<\xi VV -> (xi <= VV)>merge ([a] -> [a]<\xi VV -> (xi <= VV)>mergeSort {VV : [a] | (VV == ys) && (VV == ys) && ((len VV) == (len ys)) && ((len VV) > 0) && ((len VV) >= 0) && ((len VV) >= (len zs))}ys) ([a] -> [a]<\xi VV -> (xi <= VV)>mergeSort {VV : [a] | (VV == zs) && (VV == zs) && ((len VV) == (len zs)) && ((len VV) >= 0) && ((len VV) <= (len ys)) && ((len VV) <= (len ys))}zs) 
450:   where 
451:     ({VV : [a] | (VV == ys) && ((len VV) == (len ys)) && ((len VV) > 0) && ((len VV) >= (len zs))}ys, {VV : [a] | (VV == zs) && ((len VV) == (len zs)) && ((len VV) >= 0) && ((len VV) <= (len ys)) && ((len VV) <= (len ys))}zs)  = forall a.
x1:{VV : [a] | ((len VV) >= 0)}
-> ({VV : [a] | ((len VV) >= 0) && ((len VV) <= (len x1))}, {VV : [a] | ((len VV) >= 0) && ((len VV) <= (len x1))})<\x2 VV -> ((len x1) == ((len x2) + (len VV))) && ((len VV) >= 0) && ((len VV) <= (len x1)) && ((len VV) <= (len x2))>split {VV : [a] | ((len VV) >= 0)}xs

Lets see how LiquidHaskell proves the output type.

• The first two cases are trivial: for an empty or singleton list, we can vacuously instantiate the abstract refinement with any concrete refinement.

• For the last case, we can inductively assume mergeSort ys and mergeSort zs are sorted lists, after which the type inferred for merge kicks in, allowing LiquidHaskell to conclude that the output is also sorted.

Quick Sort

The previous two were remarkable because they were, well, quite unremarkable. Pretty much the standard textbook implementations work as is. Unlike the classical developments using indexed types we don’t have to define any auxiliary types for increasing lists, or lists whose value is in a particular range, or any specialized cons operators and so on.

With quick sort we need to do a tiny bit of work.

We would like to define quickSort as

481: {-@ quickSort'    :: (Ord a) => [a] -> IncrList a @-}
482: quickSort' []     = []
483: quickSort' (x:xs) = lts ++ (x : gts) 
484:   where 
485:     lts           = quickSort' [y | y <- xs, y < x]
486:     gts           = quickSort' [z | z <- xs, z >= x]

But, if you try it out, you’ll see that LiquidHaskell does not approve. What could possibly be the trouble?

The problem lies with append. What type do we give ++?

We might try something like

495: (++) :: IncrList a -> IncrList a -> IncrList a

but of course, this is bogus, as

499: [1,2,4] ++ [3,5,6]

is decidedly not an IncrList!

Instead, at this particular use of ++, there is an extra nugget of information: there is a pivot element x such that every element in the first argument is less than x and every element in the second argument is greater than x.

There is no way we can give the usual append ++ a type that reflects the above as there is no pivot x to refer to. Thus, with a heavy heart, we must write a specialized pivot-append that uses this fact:

516: forall a.
piv:a
-> x1:[{VV : a | (VV < piv)}]<\x3 VV -> (VV >= x3)>
-> ys:[{VV : a | (piv <= VV)}]<\x2 VV -> (x2 <= VV)>
-> {VV : [a]<\x1 VV -> (VV >= x1)> | (VV /= x1) && (VV /= ys) && ((len VV) > 0) && ((len VV) > (len x1)) && ((len VV) > (len ys))}pivApp apiv []     [{VV : a | (piv <= VV)}]<\x1 VV -> (x1 <= VV)>ys  = {VV : a | (VV == piv)}piv forall <p :: a-> a-> Bool>.
x:{VV : a | (VV >= piv)}
-> xs:[{VV : a<p x> | (VV >= piv)}]<p>
-> {VV : [{VV : a | (VV >= piv)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len xs)))}: {VV : [{VV : a | (piv <= VV)}]<\x1 VV -> (x1 <= VV)> | (VV == ys) && ((len VV) >= 0)}ys
517: pivApp piv (x:xs) ys  = {VV : a | (VV == x) && (VV < piv)}x   forall <p :: a-> a-> Bool>.
x:{VV : a | (VV >= x)}
-> xs:[{VV : a<p x> | (VV >= x)}]<p>
-> {VV : [{VV : a | (VV >= x)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len xs)))}: forall a.
piv:a
-> x1:[{VV : a | (VV < piv)}]<\x3 VV -> (VV >= x3)>
-> ys:[{VV : a | (piv <= VV)}]<\x2 VV -> (x2 <= VV)>
-> {VV : [a]<\x1 VV -> (VV >= x1)> | (VV /= x1) && (VV /= ys) && ((len VV) > 0) && ((len VV) > (len x1)) && ((len VV) > (len ys))}pivApp {VV : a | (VV == piv)}piv {VV : [{VV : a | (VV >= x) && (VV < piv)}]<\x1 VV -> (VV >= x1)> | (VV == xs) && ((len VV) >= 0)}xs {VV : [{VV : a | (piv <= VV)}]<\x1 VV -> (x1 <= VV)> | (VV == ys) && ((len VV) >= 0)}ys

Now, LiquidHaskell infers that

523: {-@ pivApp :: piv:a 
524:            -> IncrList {v:a | v <  piv} 
525:            -> IncrList {v:a | v >= piv} 
526:            -> IncrList a 
527:   @-}

And we can use pivApp to define `quickSort’ simply as:

533: {-@ quickSort    :: (Ord a) => [a] -> IncrList a @-}
534: forall a. (GHC.Classes.Ord a) => [a] -> [a]<\xi VV -> (xi <= VV)>quickSort []     = forall <p :: a-> a-> Bool>.
{VV : [{VV : a | false}]<p> | (((null VV)) <=> true) && ((len VV) == 0)}[]
535: quickSort (x:xs) = piv:a
-> [{VV : a | (VV < piv)}]<\xi VV -> (xi <= VV)>
-> [{VV : a | (VV >= piv)}]<\xi VV -> (xi <= VV)>
-> [a]<\xi VV -> (xi <= VV)>pivApp {VV : a | (VV == x)}x {VV : [{VV : a | (VV < x)}]<\xi VV -> (xi <= VV)> | (VV == lts) && ((len VV) >= 0)}lts {VV : [{VV : a | (VV >= x)}]<\xi VV -> (xi <= VV)> | (VV == gts) && ((len VV) >= 0)}gts 
536:   where 
537:     [{VV : a | (VV < x)}]<\xi VV -> (xi <= VV)>lts          = [{VV : a | (VV < x)}]
-> [{VV : a | (VV < x)}]<\xi VV -> (xi <= VV)>quickSort {VV : [{VV : a | (VV < x)}]<\_ VV -> (VV < x)> | ((len VV) >= 0) && ((len VV) <= (len xs))}[ay | y <- {VV : [a] | (VV == xs) && ((len VV) >= 0)}xs, ay x:a -> y:a -> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x < y))}< {VV : a | (VV == x)}x ]
538:     [{VV : a | (VV >= x)}]<\xi VV -> (xi <= VV)>gts          = [{VV : a | (VV >= x)}]
-> [{VV : a | (VV >= x)}]<\xi VV -> (xi <= VV)>quickSort {VV : [{VV : a | (VV >= x)}]<\_ VV -> (VV >= x)> | ((len VV) >= 0) && ((len VV) <= (len xs))}[az | z <- {VV : [a] | (VV == xs) && ((len VV) >= 0)}xs, az x:a -> y:a -> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x >= y))}>= {VV : a | (VV == x)}x]

Really Sorting Lists

The convenient thing about our encoding is that the underlying datatype is plain Haskell lists. This yields two very concrete benefits. First, as mentioned before, we can manipulate sorted lists with the same functions we’d use for regular lists. Second, by decoupling (or rather, parameterizing) the relation or property or invariant from the actual data structure we can plug in different invariants, sometimes in the same program.

To see why this is useful, lets look at a real-world sorting algorithm: the one used inside GHC’s Data.List module.

560: sort :: (Ord a) => [a] -> [a]
561: forall a. (GHC.Classes.Ord a) => [a] -> [a]<\xi VV -> (xi <= VV)>sort = {VV : [{VV : [a]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}mergeAll forall <q :: [a]-> [[a]]-> Bool, p :: [[a]]-> [a]-> Bool>.
(x:{VV : [{VV : [a]<\x5 VV -> (VV >= x5)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}
 -> {VV : [a]<\x4 VV -> (VV >= x4)><p x> | ((len VV) >= 0)})
-> (y:[a]
    -> {VV : [{VV : [a]<\x5 VV -> (VV >= x5)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)><q y> | ((len VV) > 0)})
-> x:[a]
-> exists [z:{VV : [{VV : [a]<\x5 VV -> (VV >= x5)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)><q x> | ((len VV) > 0)}].{VV : [a]<\x4 VV -> (VV >= x4)><p z> | ((len VV) >= 0)}. [a]
-> {VV : [{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}sequences
562:   where
563:     [a]
-> {VV : [{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}sequences (a:b:xs)
564:       | {VV : a | (VV == a)}a x:a
-> y:a
-> {VV : (GHC.Types.Ordering) | ((VV == GHC.Types.EQ) <=> (x == y)) && ((VV == GHC.Types.GT) <=> (x > y)) && ((VV == GHC.Types.LT) <=> (x < y))}`compare` {VV : a | (VV == b)}b x:(GHC.Types.Ordering)
-> y:(GHC.Types.Ordering)
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x == y))}== {VV : (GHC.Types.Ordering) | (VV == GHC.Types.GT) && ((cmp VV) == GHC.Types.GT)}GT = a:a
-> {VV : [{VV : a | (VV > a)}]<\x2 VV -> (VV > a) && (VV > x2)> | ((len VV) > 0)}
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}descending {VV : a | (VV == b)}b {VV : [{VV : a | (VV == a) && (VV > b)}]<\_ VV -> false> | (((null VV)) <=> false) && ((len VV) >= 0)}[{VV : a | (VV == a)}a]  {VV : [a] | (VV == xs) && ((len VV) >= 0)}xs
565:       | otherwise           = a:a
-> (x1:{VV : [{VV : a | (VV >= a)}]<\x3 VV -> (VV >= a) && (VV >= x3)> | ((len VV) > 0)}
    -> {VV : [a]<\x2 VV -> (VV >= x2)> | (VV /= x1) && ((len VV) > 0) && ((len VV) > (len x1))})
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}ascending  {VV : a | (VV == b)}b ({VV : a | (VV == a)}aforall <p :: a-> a-> Bool>.
x:{VV : a | (VV >= a)}
-> xs:[{VV : a<p x> | (VV >= a)}]<p>
-> {VV : [{VV : a | (VV >= a)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len xs)))}:) {VV : [a] | (VV == xs) && ((len VV) >= 0)}xs
566:     sequences [x] = {VV : [{VV : [{VV : a | false}]<\_ VV -> false> | false}]<\_ VV -> false> | (((null VV)) <=> true) && ((len VV) == 0) && ((len VV) >= 0)}[{VV : [{VV : a | (VV == a)}]<\_ VV -> false> | (((null VV)) <=> false) && ((len VV) >= 0)}[{VV : a | (VV == a)}x]]
567:     sequences []  = {VV : [{VV : [{VV : a | false}]<\_ VV -> false> | false}]<\_ VV -> false> | (((null VV)) <=> true) && ((len VV) == 0) && ((len VV) >= 0)}[{VV : [{VV : a | false}]<\_ VV -> false> | (((null VV)) <=> true) && ((len VV) == 0) && ((len VV) >= 0)}[]]
568: 
569:     a:a
-> {VV : [{VV : a | (VV > a)}]<\x2 VV -> (VV > a) && (VV > x2)> | ((len VV) > 0)}
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}descending aa {VV : [{VV : a | (VV > a)}]<\x1 VV -> (VV > a) && (VV > x1)> | ((len VV) > 0)}as (b:bs)
570:       | {VV : a | (VV == a)}a x:a
-> y:a
-> {VV : (GHC.Types.Ordering) | ((VV == GHC.Types.EQ) <=> (x == y)) && ((VV == GHC.Types.GT) <=> (x > y)) && ((VV == GHC.Types.LT) <=> (x < y))}`compare` {VV : a | (VV == b)}b x:(GHC.Types.Ordering)
-> y:(GHC.Types.Ordering)
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x == y))}== {VV : (GHC.Types.Ordering) | (VV == GHC.Types.GT) && ((cmp VV) == GHC.Types.GT)}GT = a:a
-> {VV : [{VV : a | (VV > a)}]<\x2 VV -> (VV > a) && (VV > x2)> | ((len VV) > 0)}
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}descending {VV : a | (VV == b)}b ({VV : a | (VV == a)}aforall <p :: a-> a-> Bool>.
x:{VV : a | (VV > b) && (VV >= a)}
-> xs:[{VV : a<p x> | (VV > b) && (VV >= a)}]<p>
-> {VV : [{VV : a | (VV > b) && (VV >= a)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len xs)))}:{VV : [{VV : a | (VV > a)}]<\x1 VV -> (VV > a) && (VV > x1)> | (VV == as) && ((len VV) > 0) && ((len VV) >= 0)}as) {VV : [a] | (VV == bs) && ((len VV) >= 0)}bs
571:     descending a as bs      = ({VV : a | (VV == a)}aforall <p :: a-> a-> Bool>.
x:{VV : a | (VV >= a)}
-> xs:[{VV : a<p x> | (VV >= a)}]<p>
-> {VV : [{VV : a | (VV >= a)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len xs)))}:{VV : [{VV : a | (VV > a)}]<\x1 VV -> (VV > a) && (VV > x1)> | (VV == as) && ((len VV) > 0) && ((len VV) >= 0)}as)forall <p :: [a]-> [a]-> Bool>.
x:{VV : [a]<\x3 VV -> (VV >= x3)> | ((len VV) >= 0)}
-> xs:[{VV : [a]<\x3 VV -> (VV >= x3)><p x> | ((len VV) >= 0)}]<p>
-> {VV : [{VV : [a]<\x3 VV -> (VV >= x3)> | ((len VV) >= 0)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len xs)))}: [a]
-> {VV : [{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}sequences {VV : [a] | ((len VV) >= 0)}bs
572: 
573:     a:a
-> (x1:{VV : [{VV : a | (VV >= a)}]<\x3 VV -> (VV >= a) && (VV >= x3)> | ((len VV) > 0)}
    -> {VV : [a]<\x2 VV -> (VV >= x2)> | (VV /= x1) && ((len VV) > 0) && ((len VV) > (len x1))})
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}ascending aa x1:{VV : [{VV : a | (VV >= a)}]<\x2 VV -> (VV >= a) && (VV >= x2)> | ((len VV) > 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | (VV /= x1) && ((len VV) > 0) && ((len VV) > (len x1))}as (b:bs)
574:       | {VV : a | (VV == a)}a x:a
-> y:a
-> {VV : (GHC.Types.Ordering) | ((VV == GHC.Types.EQ) <=> (x == y)) && ((VV == GHC.Types.GT) <=> (x > y)) && ((VV == GHC.Types.LT) <=> (x < y))}`compare` {VV : a | (VV == b)}b x:(GHC.Types.Ordering)
-> y:(GHC.Types.Ordering)
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x /= y))}/= {VV : (GHC.Types.Ordering) | (VV == GHC.Types.GT) && ((cmp VV) == GHC.Types.GT)}GT = a:a
-> (x1:{VV : [{VV : a | (VV >= a)}]<\x3 VV -> (VV >= a) && (VV >= x3)> | ((len VV) > 0)}
    -> {VV : [a]<\x2 VV -> (VV >= x2)> | (VV /= x1) && ((len VV) > 0) && ((len VV) > (len x1))})
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}ascending {VV : a | (VV == b)}b (ys:{VV : [{VV : a | (VV >= a) && (VV >= b)}]<\x2 VV -> (VV >= a) && (VV >= b) && (VV >= x2)> | ((len VV) > 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | (VV /= ys) && ((len VV) > 0) && ((len VV) > (len ys))}\{VV : [{VV : a | (VV >= a) && (VV >= b)}]<\x1 VV -> (VV >= a) && (VV >= b) && (VV >= x1)> | ((len VV) > 0)}ys -> x1:{VV : [{VV : a | (VV >= a)}]<\x2 VV -> (VV >= a) && (VV >= x2)> | ((len VV) > 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | (VV /= x1) && ((len VV) > 0) && ((len VV) > (len x1))}as ({VV : a | (VV == a)}aforall <p :: a-> a-> Bool>.
x:{VV : a | (VV >= a)}
-> xs:[{VV : a<p x> | (VV >= a)}]<p>
-> {VV : [{VV : a | (VV >= a)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len xs)))}:{VV : [{VV : a | (VV >= a) && (VV >= b)}]<\x1 VV -> (VV >= a) && (VV >= b) && (VV >= x1)> | (VV == ys) && ((len VV) > 0) && ((len VV) >= 0)}ys)) {VV : [a] | (VV == bs) && ((len VV) >= 0)}bs
575:     ascending a as bs       = x1:{VV : [{VV : a | (VV >= a)}]<\x2 VV -> (VV >= a) && (VV >= x2)> | ((len VV) > 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | (VV /= x1) && ((len VV) > 0) && ((len VV) > (len x1))}as {VV : [{VV : a | (VV == a)}]<\_ VV -> false> | (((null VV)) <=> false) && ((len VV) >= 0)}[{VV : a | (VV == a)}a]forall <p :: [a]-> [a]-> Bool>.
x:{VV : [a]<\x3 VV -> (VV >= x3)> | ((len VV) >= 0)}
-> xs:[{VV : [a]<\x3 VV -> (VV >= x3)><p x> | ((len VV) >= 0)}]<p>
-> {VV : [{VV : [a]<\x3 VV -> (VV >= x3)> | ((len VV) >= 0)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len xs)))}: [a]
-> {VV : [{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}sequences {VV : [a] | ((len VV) >= 0)}bs
576: 
577:     {VV : [{VV : [a]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}mergeAll [x] = {VV : [a]<\x1 VV -> (VV >= x1)> | (VV == x) && ((len VV) >= 0)}x
578:     mergeAll xs  = {VV : [{VV : [a]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}mergeAll (x1:{VV : [{VV : [a]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0) && ((len VV) <= (len x1))}mergePairs {VV : [{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0)}xs)
579: 
580:     x1:{VV : [{VV : [a]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0) && ((len VV) <= (len x1))}mergePairs (a:b:xs) = [a]<\xi VV -> (xi <= VV)>
-> [a]<\xi VV -> (xi <= VV)> -> [a]<\xi VV -> (xi <= VV)>merge {VV : [a]<\x1 VV -> (VV >= x1)> | (VV == a) && ((len VV) >= 0)}a {VV : [a]<\x1 VV -> (VV >= x1)> | (VV == b) && ((len VV) >= 0)}bforall <p :: [a]-> [a]-> Bool>.
x:{VV : [a]<\x3 VV -> (x3 <= VV)> | ((len VV) >= 0)}
-> xs:[{VV : [a]<\x3 VV -> (x3 <= VV)><p x> | ((len VV) >= 0)}]<p>
-> {VV : [{VV : [a]<\x3 VV -> (x3 <= VV)> | ((len VV) >= 0)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len xs)))}: x1:{VV : [{VV : [a]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0) && ((len VV) <= (len x1))}mergePairs {VV : [{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | (VV == xs) && ((len VV) >= 0)}xs
581:     mergePairs [x]      = {VV : [{VV : [{VV : a | false}]<\_ VV -> false> | false}]<\_ VV -> false> | (((null VV)) <=> true) && ((len VV) == 0) && ((len VV) >= 0)}[{VV : [a]<\x1 VV -> (VV >= x1)> | (VV == a) && ((len VV) >= 0)}x]
582:     mergePairs []       = forall <p :: [a]-> [a]-> Bool>.
{VV : [{VV : [{VV : a | false}]<\_ VV -> false> | false}]<p> | (((null VV)) <=> true) && ((len VV) == 0)}[]

The interesting thing about the procedure is that it generates some intermediate lists that are increasing and others that are decreasing, and then somehow miraculously whips this whirlygig into a single increasing list.

Yet, to check this rather tricky algorithm with LiquidHaskell we need merely write:

595: {-@ sort :: (Ord a) => [a] -> IncrList a  @-}

---