Regarding reverse in Ch 8: Sets

[hafizhmakmur]

There is an exercise in Ch 8 where we need to fix this function

{-@ reverse    :: xs:UList a -> UList a    @-}
reverse         = go []
  where
    {-@ go     :: acc:[a] -> xs:[a] -> [a] @-}
    go acc []     = acc
    go acc (x:xs) = go (x:acc) xs

First I tried to solve it and I come up with a nice specification which I thought suffices to be the answer

{-@ reverse    :: xs:UList a -> UList a @-}
reverse :: [a] -> [a]
reverse         = go []
  where
    {-@ go     :: acc:UList a -> {xs:UList a | Disj acc xs} 
                              -> {v:UList a | Union (elts v)
                                                    (elts acc)
                                                    (elts xs)} @-}
    go :: [a] -> [a] -> [a]
    go acc []     = acc
    go acc (x:xs) = go (x:acc) xs

Then I stumble into this article which explains it a little bit differently. In it there's what essentially the answer for this exercise, which very surprisingly is as simple as (rephrased)

{-@ reverse    :: xs:UList a -> UList a    @-}
reverse         = go []
  where
    --{-@ go     :: acc:[a] -> xs:[a] -> [a] @-}
    go acc []     = acc
    go acc (x:xs) = go (x:acc) xs

In other words, commenting out the specification for go lets LH to create a fitting specification by itself and instead save us the effort to write the specification by ourselves.

Is it really the intended answer? I feel like there's an important lesson of letting LH works by itself which I won't get at all if I don't stumble into that article, instead it makes me create the specification myself, which is a good exercise, but after seeing this I don't think now that it's really intended. I have tried to comment out specifications for other intermediary functions and it works well. I think maybe the tutorial maybe needs to explain this bit somewhere in the tutorial because I don't think letting users to do unnecessary work is what we really wanted especially looking at some of LH articles where LH pride itself in making user write as few specifications as possible.

[ranjitjhala]

Dear Hafizh,

you raise a good point. This is a somewhat philosophical issue of course.

You are right that we do want to make the user write as few specs as possible.

However, this is in tension with the goal of the tutorial which is indeed to help understand how to use LH, and for which I have found practice with writing specifications is extremely useful.

This is why we have left it in as an exercise, even though in practice LH can infer this particular specification automatically.

Does that help? However, you are right - maybe I should make this point very clearly and explicitly in the tutorial itself!

If you like, would you like to submit a small PR that adds such a paragraph (essentially your email but without the "link" to the blog post, just saying "in practice LH can infer the specification but we leave this to the reader as an exercise").

(of course, no worries if you can't I will add it myself!)

Many thanks again!!!

• Ranjit.

On Mon, Jun 15, 2020 at 6:39 AM Hafizh Afkar Makmur < notifications@github.com> wrote:

There is an exercise in Ch 8 where we need to fix this function

{-@ reverse :: xs:UList a -> UList a @-} reverse = go [] where {-@ go :: acc:[a] -> xs:[a] -> [a] @-} go acc [] = acc go acc (x:xs) = go (x:acc) xs

First I tried to solve it and I come up with a nice specification which I thought suffices to be the answer

{-@ reverse :: xs:UList a -> UList a @-} reverse :: [a] -> [a] reverse = go [] where {-@ go :: acc:UList a -> {xs:UList a | Disj acc xs} -> {v:UList a | Union (elts v) (elts acc) (elts xs)} @-} go :: [a] -> [a] -> [a] go acc [] = acc go acc (x:xs) = go (x:acc) xs

Then I stumble into this article https://urldefense.com/v3/__https://ucsd-progsys.github.io/liquidhaskell-blog/2013/05/24/unique-zipper.lhs/__;!!Mih3wA!SoXyIpTJRYjSAZVhLgRu6S7q6_BTtcPSOElN16L0fXvVTzgl4vjX1wcGwHsBxZ8T$ which explains it a little bit differently. In it there's what essentially the answer for this exercise, which very surprisingly is as simple as (rephrased)

{-@ reverse :: xs:UList a -> UList a @-} reverse = go [] where --{-@ go :: acc:[a] -> xs:[a] -> [a] @-} go acc [] = acc go acc (x:xs) = go (x:acc) xs

In other words, commenting out the specification for go lets LH to create a fitting specification by itself and instead save us the effort to write the specification by ourselves.

Is it really the intended answer? I feel like there's an important lesson of letting LH works by itself which I won't get at all if I don't stumble into that article, instead it makes me create the specification myself, which is a good exercise, but after seeing this I don't think now that it's really intended. I have tried to comment out specifications for other intermediary functions and it works well. I think maybe the tutorial maybe needs to explain this bit somewhere in the tutorial because I don't think letting users to do unnecessary work is what we really wanted especially looking at some of LH articles where LH pride itself in making user write as few specifications as possible.

— 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/100__;!!Mih3wA!SoXyIpTJRYjSAZVhLgRu6S7q6_BTtcPSOElN16L0fXvVTzgl4vjX1wcGwBlL9TRB$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OASD3PJLYBF2GE3LVLRWYQCFANCNFSM4N6GBKVQ__;!!Mih3wA!SoXyIpTJRYjSAZVhLgRu6S7q6_BTtcPSOElN16L0fXvVTzgl4vjX1wcGwKBLVNHP$ .

[hafizhmakmur]

Thank you very much for your response! I was just asking this to confirm my understanding of the material and your answer helps very much! Maybe I'll make some compilation of parts that I think can be made easier for readers to understand (at least for me!) and create a complete PR but for now I want to be really sure first about my understanding about this tutorial.