Putting Things In Order
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 between0
and9
- In
sparseVecP
the keys are between0
and999
.
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 ofp
as a binary relation over thea
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 byp
. -
The cons constructor
(:)
takes a headh
of typea
and a tail ofa<p h>
values, each of which is related toh
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
andmergeSort zs
are sorted lists, after which the type inferred formerge
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 @-}