Issues with quickSort in chapter 6 #79
Comments
skyzh
changed the title
skyzh
changed the title
|
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 ***@***.***> 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
<#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 ***@***.***> 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 ***@***.***> 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
> <#79>, or mute
> the thread
> <https://github.com/notifications/unsubscribe-auth/ABkuOA8YXdTX67XcotN8eqqdQb6OASB0ks5vN5KKgaJpZM4a-yhy>
> .
>
|
|
Thank you for your response! I've just figured out a working example by defining https://github.com/SkyZH/introliquid.hs/blob/master/src/Ex06.hs#L150 |
|
Excellent!!
…On Fri, Feb 15, 2019 at 9:33 PM Alex Chi ***@***.***> 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
<#79 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/ABkuOPa1l1BfIL46FG5wXW6h5oqwuvDWks5vN5gIgaJpZM4a-yhy>
.
|
|
I've missed your first reply...
{-@ measure size @-}
{-@ size :: xs:[a] -> {v:Nat | v = len xs} @-}
size :: [a] -> Int
size [] = 0
size (_:rs) = 1 + size rs
|
{-@ 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 rswhich yields exactly the same error. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Hello! I encountered some problems when I was trying solving exercise 6.6
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' rWhich I got the following error:
And I suspect that Liquid Haskell may fail to deduce the
sizeof 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 ++ bAnd certainly I got the following error:
Is there anyway to make Liquid Haskell deduce that
++can correctly add up size?Thank you for reading this issue!
The text was updated successfully, but these errors were encountered: