search

ucsd-progsys / liquidhaskell-tutorial

Tutorial for LiquidHaskell
https://ucsd-progsys.github.io/liquidhaskell-tutorial/
MIT License
75 stars 27 forks source link

Trouble with Chapter 11 #98

Closed hafizhmakmur closed 4 years ago

hafizhmakmur commented 4 years ago

First I'd like to inform that the signature for mallocForeignPtrBytes :: Int -> ForeignPtr a is wrong. It should be mallocForeignPtrBytes :: Int -> IO (ForeignPtr a) which strangely is right in the source code but not in the tutorial text.

Second, as seen in this code, I'm already very sure that I have made a right create function so that bsGHC is deemed as correct but somehow the pack function after that is still deemed wrong.

I have also looked at the source code of the create' function and it's the same and create is also deemed right when I type it into the website so it seems that there's some auxiliary code that I have to type but I haven't. It also affects any next practices so I think I need to know what's wrong with this before I move on.

hafizhmakmur commented 4 years ago

After copying lots of codes I don't understand from the source code and going further, I am finally able to make the code all safe except for one, as seen in this code. Here somehow chop is still deemed unsafe because of b' = unsafeTake n b and I don't know why. I dont think there's any more helper code I can copy to fix this so how can I fix this code and make it safe?

ranjitjhala commented 4 years ago

(Thanks for pointing out the typo in the informal text for mallocForeignPtrBytes -- will fix!)

The spec for unsafeTake has some precondition about bOff which is not established by pack.

A hint: the type for unsafeTake is much simpler -- you can write it without referring to bOff and only using the bLen.

Try to work it out (you're very close) -- but if not, click below

http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1591367347_9690.hs

On Thu, Jun 4, 2020 at 8:35 AM Hafizh Afkar Makmur notifications@github.com wrote:

After copying lots of codes I don't understand from the source code and going further, I am finally able to make the code all safe except for one, as seen in this code http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1591284714_9660.hs. Here somehow chop is still deemed unsafe because of b' = unsafeTake n b and I don't know why. I dont think there's any more helper code I can copy to fix this so how can I fix this code and make it safe?

— 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/98*issuecomment-638928795__;Iw!!Mih3wA!Vs8-M4fBaSatEoDuX89s1LRMEod7UQIONCecmpcb8sS7a9SVPRQlelDMfQbLugbK$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OH5FLWLMTOMF2K37TDRU65KLANCNFSM4NSKSR4Q__;!!Mih3wA!Vs8-M4fBaSatEoDuX89s1LRMEod7UQIONCecmpcb8sS7a9SVPRQlelDMfRIaeSoH$ .

hafizhmakmur commented 4 years ago

Thank you very much! I see that the function ignores the bLen entirely so I never thought that bLen would be used in the specification. :D Once again thank you very much!

NB: In Figure 12.5 the most left triangle should be "ll" not "lr". Also I can't run Chapter 10 page entirely because of some missing imports that I can't repair because the code also don't recognize import. @ranjitjhala