Issues with quickSort in chapter 6

Hello! I encountered some problems when I was trying solving exercise 6.6

Exercise 6.6 (QuickSort). Use partition to implement quickSort.
-- >> quickSort [1,4,3,2] 
-- [1,2,3,4] 
{-@ quickSort :: (Ord a) => xs:List a -> ListX a xs @-} 
quickSort [] = [] 
quickSort (x:xs) = undefined 
{-@ test10 :: ListN String 2 @-} 
test10 = quickSort test4

Here's my implementation:

{-@ partition :: _ -> xs:_ -> {v:_ | Sum2 v (size xs)} @-}
{-@ predicate Sum2 X N = size (fst X) + size (snd X) = N @-}

partition :: (a -> Bool) -> [a] -> ([a], [a])
partition _ [] = ([], [])
partition f (x:xs)
  | f x = (x:ys, zs)
  | otherwise = (ys, x:zs)
  where
    (ys, zs) = partition f xs

-- exercise 6.6
{-@ quickSort' :: (Ord a) => xs:List a -> ListX a xs @-}
quickSort' :: (Ord a) => [a] -> [a]
quickSort' [] = []
quickSort' (x:xs) = let
  (l, r) = partition cmp xs
  cmp t = t < x in
     quickSort' l ++ [x] ++ quickSort' r

Which I got the following error:

 /Users/skyzh/Work/playground/src/Ex06.hs:152:6-17: Error: Liquid Type Mismatch

 152 |      quickSort' l ++ [x] ++ quickSort' r
            ^^^^^^^^^^^^

   Inferred type
     VV : {v : [a##xo] | len v >= 0
                         && v == fst ?a
                         && v /= ?b
                         && Ex06.size v >= 0}

   not a subtype of Required type
     VV : {VV : [a##xo] | len VV < len ?b
                          && len VV >= 0}

   In Context
     xs : {v : [a##xo] | Ex06.size v >= 0
                         && len v >= 0}

     ?b : {?b : [a##xo] | Ex06.size ?b >= 0
                          && len ?b >= 0}

     x : a##xo

     ?a : {?a : ([a##xo], [a##xo]) | Ex06.size (fst ?a) + Ex06.size (snd ?a) == Ex06.size xs}

 /Users/skyzh/Work/playground/src/Ex06.hs:152:6-40: Error: Liquid Type Mismatch

 152 |      quickSort' l ++ [x] ++ quickSort' r
            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

   Inferred type
     VV : {v : [a##xo] | len v == len ?f + len ?b
                         && Ex06.size v >= 0
                         && len v >= 0}

   not a subtype of Required type
     VV : {VV : [a##xo] | Ex06.size VV == Ex06.size ?e}

   In Context
     ?g : {?g : [a##xo] | (Ex06.notEmpty ?g <=> false)
                          && Ex06.size ?g == 0
                          && len ?g == 0
                          && Ex06.size ?g >= 0
                          && len ?g >= 0}

     xs : {v : [a##xo] | Ex06.size v >= 0
                         && len v >= 0}

     ?f : {?f : [a##xo] | Ex06.size ?f == Ex06.size (fst ?c)
                          && Ex06.size ?f >= 0
                          && len ?f >= 0}

     ?c : {?c : ([a##xo], [a##xo]) | Ex06.size (fst ?c) + Ex06.size (snd ?c) == Ex06.size xs}

     ?e : {?e : [a##xo] | Ex06.size ?e >= 0
                          && len ?e >= 0}

     ?b : {?b : [a##xo] | len ?b == len ?a + len ?d
                          && Ex06.size ?b >= 0
                          && len ?b >= 0}

     x : a##xo

     ?d : {?d : [a##xo] | Ex06.size ?d == Ex06.size (snd ?c)
                          && Ex06.size ?d >= 0
                          && len ?d >= 0}

     ?a : {?a : [a##xo] | tail ?a == ?g
                          && head ?a == x
                          && (Ex06.notEmpty ?a <=> true)
                          && Ex06.size ?a == 1 + Ex06.size ?g
                          && len ?a == 1 + len ?g
                          && Ex06.size ?a >= 0
                          && len ?a >= 0}

 /Users/skyzh/Work/playground/src/Ex06.hs:152:29-40: Error: Liquid Type Mismatch

 152 |      quickSort' l ++ [x] ++ quickSort' r
                                   ^^^^^^^^^^^^

   Inferred type
     VV : {v : [a##xo] | len v >= 0
                         && v == snd ?a
                         && v /= ?b
                         && Ex06.size v >= 0}

   not a subtype of Required type
     VV : {VV : [a##xo] | len VV < len ?b
                          && len VV >= 0}

   In Context
     xs : {v : [a##xo] | Ex06.size v >= 0
                         && len v >= 0}

     ?b : {?b : [a##xo] | Ex06.size ?b >= 0
                          && len ?b >= 0}

     x : a##xo

     ?a : {?a : ([a##xo], [a##xo]) | Ex06.size (fst ?a) + Ex06.size (snd ?a) == Ex06.size xs}

And I suspect that Liquid Haskell may fail to deduce the size of operator ++. Then I made an experiment to test.

{-@ (+++) :: xs: List a -> ys: List a -> ListN a {size xs + size ys} @-}
(+++) :: [a] -> [a] -> [a]
a +++ b = a ++ b

And certainly I got the following error:

/Users/skyzh/Work/playground/src/Ex06.hs:143:11-16: Error: Liquid Type Mismatch

 143 | a +++ b = a ++ b
                 ^^^^^^

   Inferred type
     VV : {v : [a##xo] | len v == len a + len b
                         && Ex06.size v >= 0
                         && len v >= 0}

   not a subtype of Required type
     VV : {VV : [a##xo] | Ex06.size VV == Ex06.size a + Ex06.size b}

   In Context
     a : {a : [a##xo] | Ex06.size a >= 0
                        && len a >= 0}

     b : {b : [a##xo] | Ex06.size b >= 0
                        && len b >= 0}

Is there anyway to make Liquid Haskell deduce that ++ can correctly add up size?

Thank you for reading this issue!

I've also tested my code on the online version, which caused the same issue. http://ucsd-progsys.github.io/liquidhaskell-tutorial/07-measure-int.html#/program-40

thanks for posting this!

Indeed The issue here is that ++ is defined using “Len” not “size”.

Two solutions:

1 use “Len” instead of “size” In the spec of “partition”

2 tell LH that “Len” is the same as “size” by specifying that

Size :: xs:_ -> {v:Nat| v= Len xs}

Does that help?

output type of size :: You can tell LH that len and size are the same th

On Fri, Feb 15, 2019 at 9:10 PM Alex Chi notifications@github.com wrote:

Hello! I encountered some problems when I was trying solving exercise 6.6

Exercise 6.6 (QuickSort). Use partition to implement quickSort. -- >> quickSort [1,4,3,2] -- [1,2,3,4] {-@ quickSort :: (Ord a) => xs:List a -> ListX a xs @-} quickSort [] = [] quickSort (x:xs) = undefined {-@ test10 :: ListN String 2 @-} test10 = quickSort test4

Here's my implementation:

{-@ partition :: -> xs: -> {v: | Sum2 v (size xs)} @-} {-@ predicate Sum2 X N = size (fst X) + size (snd X) = N @-} partition :: (a -> Bool) -> [a] -> ([a], [a]) partition [] = ([], []) partition f (x:xs) | f x = (x:ys, zs) | otherwise = (ys, x:zs) where (ys, zs) = partition f xs -- exercise 6.6 {-@ quickSort' :: (Ord a) => xs:List a -> ListX a xs @-}quickSort' :: (Ord a) => [a] -> [a] quickSort' [] = [] quickSort' (x:xs) = let (l, r) = partition cmp xs cmp t = t < x in quickSort' l ++ [x] ++ quickSort' r

Which I got the following error:

/Users/skyzh/Work/playground/src/Ex06.hs:152:6-17: Error: Liquid Type Mismatch

152 | quickSort' l ++ [x] ++ quickSort' r ^^^^^^^^^^^^

Inferred type VV : {v : [a##xo] | len v >= 0 && v == fst ?a && v /= ?b && Ex06.size v >= 0}

not a subtype of Required type VV : {VV : [a##xo] | len VV < len ?b && len VV >= 0}

In Context xs : {v : [a##xo] | Ex06.size v >= 0 && len v >= 0}
 ?b : {?b : [a##xo] | Ex06.size ?b >= 0
                      && len ?b >= 0}

 x : a##xo

 ?a : {?a : ([a##xo], [a##xo]) | Ex06.size (fst ?a) + Ex06.size (snd ?a) == Ex06.size xs}
/Users/skyzh/Work/playground/src/Ex06.hs:152:6-40: Error: Liquid Type Mismatch

152 | quickSort' l ++ [x] ++ quickSort' r ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Inferred type VV : {v : [a##xo] | len v == len ?f + len ?b && Ex06.size v >= 0 && len v >= 0}

not a subtype of Required type VV : {VV : [a##xo] | Ex06.size VV == Ex06.size ?e}

In Context ?g : {?g : [a##xo] | (Ex06.notEmpty ?g <=> false) && Ex06.size ?g == 0 && len ?g == 0 && Ex06.size ?g >= 0 && len ?g >= 0}
 xs : {v : [a##xo] | Ex06.size v >= 0
                     && len v >= 0}

 ?f : {?f : [a##xo] | Ex06.size ?f == Ex06.size (fst ?c)
                      && Ex06.size ?f >= 0
                      && len ?f >= 0}

 ?c : {?c : ([a##xo], [a##xo]) | Ex06.size (fst ?c) + Ex06.size (snd ?c) == Ex06.size xs}

 ?e : {?e : [a##xo] | Ex06.size ?e >= 0
                      && len ?e >= 0}

 ?b : {?b : [a##xo] | len ?b == len ?a + len ?d
                      && Ex06.size ?b >= 0
                      && len ?b >= 0}

 x : a##xo

 ?d : {?d : [a##xo] | Ex06.size ?d == Ex06.size (snd ?c)
                      && Ex06.size ?d >= 0
                      && len ?d >= 0}

 ?a : {?a : [a##xo] | tail ?a == ?g
                      && head ?a == x
                      && (Ex06.notEmpty ?a <=> true)
                      && Ex06.size ?a == 1 + Ex06.size ?g
                      && len ?a == 1 + len ?g
                      && Ex06.size ?a >= 0
                      && len ?a >= 0}
/Users/skyzh/Work/playground/src/Ex06.hs:152:29-40: Error: Liquid Type Mismatch

152 | quickSort' l ++ [x] ++ quickSort' r ^^^^^^^^^^^^

Inferred type VV : {v : [a##xo] | len v >= 0 && v == snd ?a && v /= ?b && Ex06.size v >= 0}

not a subtype of Required type VV : {VV : [a##xo] | len VV < len ?b && len VV >= 0}

In Context xs : {v : [a##xo] | Ex06.size v >= 0 && len v >= 0}
 ?b : {?b : [a##xo] | Ex06.size ?b >= 0
                      && len ?b >= 0}

 x : a##xo

 ?a : {?a : ([a##xo], [a##xo]) | Ex06.size (fst ?a) + Ex06.size (snd ?a) == Ex06.size xs}
And I suspect that Liquid Haskell may fail to deduce the size of operator ++. Then I made an experiment to test.

{-@ (+++) :: xs: List a -> ys: List a -> ListN a {size xs + size ys} @-}(+++) :: [a] -> [a] -> [a] a +++ b = a ++ b

And certainly I got the following error:

/Users/skyzh/Work/playground/src/Ex06.hs:143:11-16: Error: Liquid Type Mismatch

143 | a +++ b = a ++ b ^^^^^^

Inferred type VV : {v : [a##xo] | len v == len a + len b && Ex06.size v >= 0 && len v >= 0}

not a subtype of Required type VV : {VV : [a##xo] | Ex06.size VV == Ex06.size a + Ex06.size b}

In Context a : {a : [a##xo] | Ex06.size a >= 0 && len a >= 0}
 b : {b : [a##xo] | Ex06.size b >= 0
                    && len b >= 0}
Is there anyway to make Liquid Haskell deduce that ++ can correctly add up size?

Thank you for reading this issue!

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/79, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOA8YXdTX67XcotN8eqqdQb6OASB0ks5vN5KKgaJpZM4a-yhy .

But this is not something you should have to worry about for this exercise — I think some of the LH defaults have changed since I wrote it so don’t close the issue, I’ll fix the tutorial.

Than again!

On Fri, Feb 15, 2019 at 9:25 PM Ranjit Jhala jhala@cs.ucsd.edu wrote:

thanks for posting this!

Indeed The issue here is that ++ is defined using “Len” not “size”.

Two solutions:

1 use “Len” instead of “size” In the spec of “partition”

2 tell LH that “Len” is the same as “size” by specifying that

Size :: xs:_ -> {v:Nat| v= Len xs}

Does that help?

output type of size :: You can tell LH that len and size are the same th

On Fri, Feb 15, 2019 at 9:10 PM Alex Chi notifications@github.com wrote:
Hello! I encountered some problems when I was trying solving exercise 6.6

Exercise 6.6 (QuickSort). Use partition to implement quickSort. -- >> quickSort [1,4,3,2] -- [1,2,3,4] {-@ quickSort :: (Ord a) => xs:List a -> ListX a xs @-} quickSort [] = [] quickSort (x:xs) = undefined {-@ test10 :: ListN String 2 @-} test10 = quickSort test4

Here's my implementation:

{-@ partition :: -> xs: -> {v: | Sum2 v (size xs)} @-} {-@ predicate Sum2 X N = size (fst X) + size (snd X) = N @-} partition :: (a -> Bool) -> [a] -> ([a], [a]) partition [] = ([], []) partition f (x:xs) | f x = (x:ys, zs) | otherwise = (ys, x:zs) where (ys, zs) = partition f xs -- exercise 6.6 {-@ quickSort' :: (Ord a) => xs:List a -> ListX a xs @-}quickSort' :: (Ord a) => [a] -> [a] quickSort' [] = [] quickSort' (x:xs) = let (l, r) = partition cmp xs cmp t = t < x in quickSort' l ++ [x] ++ quickSort' r

Which I got the following error:

/Users/skyzh/Work/playground/src/Ex06.hs:152:6-17: Error: Liquid Type Mismatch

152 | quickSort' l ++ [x] ++ quickSort' r ^^^^^^^^^^^^

Inferred type VV : {v : [a##xo] | len v >= 0 && v == fst ?a && v /= ?b && Ex06.size v >= 0}

not a subtype of Required type VV : {VV : [a##xo] | len VV < len ?b && len VV >= 0}

In Context xs : {v : [a##xo] | Ex06.size v >= 0 && len v >= 0}
 ?b : {?b : [a##xo] | Ex06.size ?b >= 0
                      && len ?b >= 0}

 x : a##xo

 ?a : {?a : ([a##xo], [a##xo]) | Ex06.size (fst ?a) + Ex06.size (snd ?a) == Ex06.size xs}
/Users/skyzh/Work/playground/src/Ex06.hs:152:6-40: Error: Liquid Type Mismatch

152 | quickSort' l ++ [x] ++ quickSort' r ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Inferred type VV : {v : [a##xo] | len v == len ?f + len ?b && Ex06.size v >= 0 && len v >= 0}

not a subtype of Required type VV : {VV : [a##xo] | Ex06.size VV == Ex06.size ?e}

In Context ?g : {?g : [a##xo] | (Ex06.notEmpty ?g <=> false) && Ex06.size ?g == 0 && len ?g == 0 && Ex06.size ?g >= 0 && len ?g >= 0}
 xs : {v : [a##xo] | Ex06.size v >= 0
                     && len v >= 0}

 ?f : {?f : [a##xo] | Ex06.size ?f == Ex06.size (fst ?c)
                      && Ex06.size ?f >= 0
                      && len ?f >= 0}

 ?c : {?c : ([a##xo], [a##xo]) | Ex06.size (fst ?c) + Ex06.size (snd ?c) == Ex06.size xs}

 ?e : {?e : [a##xo] | Ex06.size ?e >= 0
                      && len ?e >= 0}

 ?b : {?b : [a##xo] | len ?b == len ?a + len ?d
                      && Ex06.size ?b >= 0
                      && len ?b >= 0}

 x : a##xo

 ?d : {?d : [a##xo] | Ex06.size ?d == Ex06.size (snd ?c)
                      && Ex06.size ?d >= 0
                      && len ?d >= 0}

 ?a : {?a : [a##xo] | tail ?a == ?g
                      && head ?a == x
                      && (Ex06.notEmpty ?a <=> true)
                      && Ex06.size ?a == 1 + Ex06.size ?g
                      && len ?a == 1 + len ?g
                      && Ex06.size ?a >= 0
                      && len ?a >= 0}
/Users/skyzh/Work/playground/src/Ex06.hs:152:29-40: Error: Liquid Type Mismatch

152 | quickSort' l ++ [x] ++ quickSort' r ^^^^^^^^^^^^

Inferred type VV : {v : [a##xo] | len v >= 0 && v == snd ?a && v /= ?b && Ex06.size v >= 0}

not a subtype of Required type VV : {VV : [a##xo] | len VV < len ?b && len VV >= 0}

In Context xs : {v : [a##xo] | Ex06.size v >= 0 && len v >= 0}
 ?b : {?b : [a##xo] | Ex06.size ?b >= 0
                      && len ?b >= 0}

 x : a##xo

 ?a : {?a : ([a##xo], [a##xo]) | Ex06.size (fst ?a) + Ex06.size (snd ?a) == Ex06.size xs}
And I suspect that Liquid Haskell may fail to deduce the size of operator ++. Then I made an experiment to test.

{-@ (+++) :: xs: List a -> ys: List a -> ListN a {size xs + size ys} @-}(+++) :: [a] -> [a] -> [a] a +++ b = a ++ b

And certainly I got the following error:

/Users/skyzh/Work/playground/src/Ex06.hs:143:11-16: Error: Liquid Type Mismatch

143 | a +++ b = a ++ b ^^^^^^

Inferred type VV : {v : [a##xo] | len v == len a + len b && Ex06.size v >= 0 && len v >= 0}

not a subtype of Required type VV : {VV : [a##xo] | Ex06.size VV == Ex06.size a + Ex06.size b}

In Context a : {a : [a##xo] | Ex06.size a >= 0 && len a >= 0}
 b : {b : [a##xo] | Ex06.size b >= 0
                    && len b >= 0}
Is there anyway to make Liquid Haskell deduce that ++ can correctly add up size?

Thank you for reading this issue!

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/79, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOA8YXdTX67XcotN8eqqdQb6OASB0ks5vN5KKgaJpZM4a-yhy .

Excellent!!

On Fri, Feb 15, 2019 at 9:33 PM Alex Chi notifications@github.com wrote:

Thank you for your response! I've just figured out a working example by defining pivApp similar to http://goto.ucsd.edu/~gridaphobe/liquid/haskell/blog/blog/2013/07/29/putting-things-in-order.lhs/

https://github.com/SkyZH/introliquid.hs/blob/master/src/Ex06.hs#L150

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/79#issuecomment-464294543, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOPa1l1BfIL46FG5wXW6h5oqwuvDWks5vN5gIgaJpZM4a-yhy .

I've missed your first reply...

use “Len” instead of “size” In the spec of “partition” does not help, because ListN is defined by size...
tell LH that “Len” is the same as “size” by specifying that does not help.

{-@ measure size @-}
{-@ size :: xs:[a] -> {v:Nat | v = len xs} @-}
size :: [a] -> Int
size [] = 0
size (_:rs) = 1 + size rs

/Users/skyzh/Work/playground/src/Ex06.hs:157:5-17: Error: Liquid Type Mismatch

 157 |     l ++ [x] ++ r
           ^^^^^^^^^^^^^

   Inferred type
     VV : {v : [a##xo] | len v == len (Ex06.fst ?f) + len ?b
                         && Ex06.size v >= 0
                         && len v >= 0}

   not a subtype of Required type
     VV : {VV : [a##xo] | Ex06.size VV == Ex06.size ?e}

   In Context
     xs : {v : [a##xo] | Ex06.size v >= 0
                         && len v >= 0}

     ?f : {?f : ([a##xo], [a##xo]) | Ex06.size (fst ?f) + Ex06.size (snd ?f) == Ex06.size xs
                                     && len (fst ?f) + len (snd ?f) == Ex06.size xs}

     ?c : {?c : [a##xo] | tail ?c == ?a
                          && head ?c == x
                          && (Ex06.notEmpty ?c <=> true)
                          && Ex06.size ?c == 1 + Ex06.size ?a
                          && len ?c == 1 + len ?a
                          && Ex06.size ?c >= 0
                          && len ?c >= 0}

     ?e : {?e : [a##xo] | Ex06.size ?e >= 0
                          && len ?e >= 0}

     ?b : {?b : [a##xo] | len ?b == len ?c + len (Ex06.snd ?f)
                          && Ex06.size ?b >= 0
                          && len ?b >= 0}

     x : a##xo

     ?a : {?a : [a##xo] | (Ex06.notEmpty ?a <=> false)
                          && Ex06.size ?a == 0
                          && len ?a == 0
                          && Ex06.size ?a >= 0
                          && len ?a >= 0}

replace all size with len this is ok 💯, here's the working example https://github.com/SkyZH/introliquid.hs/blob/master/src/Ex06len.hs

tell LH that “Len” is the same as “size” by specifying that still does not help if I change the definition from the one in the previous comment into:

  {-@ measure size @-}
- {-@ size :: xs::[a]-> {v:Nat | v = len xs} @-}
+ {-@ size :: xs:_ -> {v:Nat | v = len xs} @-}
  size :: [a] -> Int
  size [] = 0
  size (_:rs) = 1 + size rs

which yields exactly the same error.

ucsd-progsys / liquidhaskell-tutorial

Issues with quickSort in chapter 6 #79