Why does this zipWith from Chapter 7 fails?

[hafizhmakmur]

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]

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 < notifications@github.com> 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]

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]

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 < notifications@github.com> 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$ .