Why does this zipWith from Chapter 7 fails?
hafizhmakmur opened this issue · 3 comments
hafizhmakmur commented
I'm trying the codes from Chapter 7 in this code and somehow here all the zip functions fail. Is there anything missing that would make these functions safe?
Additional Note: I also have to comment out the DotProd
function because it uses a different zipWith with the one that is written later in the code hence it will fail since built-in zipWith
doesn't need its parameters to have the same size.
ranjitjhala commented
Sorry! The reason the tests fail is _very_ tricky.
Your code was just missing the one fact that
{-@ size :: [a] -> Nat @-}
which says that `size xs` is always **non-negative**
This seems simple but actually is very important!
Without this information LH can think that
an arbitrary list `xs` length is -5 which
throws off the verification.
http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1590335576_9225.hs
Actually, this is an *excellent* question you have asked.
(Something that as the "implementor" I have taken for
granted, without thinking clearly about how to explain
what is going on. Let me think properly about an explanation
that I can then write up nicely, MANY thanks for posting this example!!!)
…On Fri, May 22, 2020 at 12:27 AM Hafizh Afkar Makmur < ***@***.***> wrote:
I'm trying the codes from Chapter 7 in this code
<http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1590132075_9135.hs>
and somehow here all the zip functions fail. Is there anything missing that
would make these functions safe?
Additional Note: I also have to comment out the DotProd function because
it uses a different zipWith with the one that is written later in the code
hence it will fail since built-in zipWith doesn't need its parameters to
have the same size.
—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
<https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/96__;!!Mih3wA!RTDkCXTr6_kX6iVwlL8OudY9UTLdvI80OP_3evSZgkTfuyvQW_Ye6-9OhO8ZVKu5$>,
or unsubscribe
<https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OGPOTAVQT63SFQ7PRTRSYSMHANCNFSM4NHRW3SQ__;!!Mih3wA!RTDkCXTr6_kX6iVwlL8OudY9UTLdvI80OP_3evSZgkTfuyvQW_Ye6-9OhFktmKbN$>
.
hafizhmakmur commented
Thank you very much for your response! I was very confused because the webpage somehow compiles nicely when I just copied some code and it fails. Also I have checked the .lhs file and there's no {-@ size :: [a] -> Nat @-}
so I'm quite confused why it's deemed safe? Once again, thank you very much!
ranjitjhala commented
Aha good question!
In fact if you look at the LHS it has this line
https://github.com/ucsd-progsys/liquidhaskell-tutorial/blob/master/src/07-measure-int.lhs#L22
Which (is old, deprecated syntax that) basically says the same thing as
size :: [a] -> Nat
Namely the size of any list is non negative.
…On Sun, May 24, 2020 at 6:16 PM Hafizh Afkar Makmur < ***@***.***> wrote:
Thank you very much for your response! I was very confused because the
webpage somehow compiles nicely when I just copied some code and it fails.
Also I have checked the .lhs file and there's no {-@ size :: [a] -> Nat
@-} so I'm quite confused why it's deemed safe? Once again, thank you
very much!
—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
<https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/96*issuecomment-633331692__;Iw!!Mih3wA!S3GAi8pUsQndvpdGLfnL6CBKsDlIYfaaTReydw-qvOm5Pa1JWYOa19hQGPzeuYvR$>,
or unsubscribe
<https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OEXEAXUTGP6THN2TEDRTHBF5ANCNFSM4NHRW3SQ__;!!Mih3wA!S3GAi8pUsQndvpdGLfnL6CBKsDlIYfaaTReydw-qvOm5Pa1JWYOa19hQGFHf0iTu$>
.