How do you refine a predicate which checks over all elements in a list?

[hafizhmakmur]

I'm trying to write a specification for a function that checks over all elements in a list. For example what I'm trying to refine is a simple function like this

isOver :: Int -> [Int] -> Bool
isOver lo xs 
    | length xs == 0 = True
    | (lo < (head xs)) = isOver lo (tail xs)
    | otherwise = False

As can be seen isOver should be a function that checks whether all elements in the list are over some input and then returns True or False. It can of course also be implemented like this

isOver :: Int -> [Int] -> Bool
isOver lo = foldl (\acc x -> acc && (lo < x)) True 

How do I write a specification to check whether either implementation is safe? Or this kind of predicate cannot be written the specification and instead only assumed as true and be used as measure?

[ranjitjhala]

There are various ways to write such a spec but what are you trying to do with this specification? (That will help me understand what is suitable.)

You can write specs of the below kind using “reflection” (which unfortunately is not covered in the tutorial yet).

On Wed, May 20, 2020 at 5:10 PM Hafizh Afkar Makmur < notifications@github.com> wrote:

I'm trying to write a specification for a function that checks over all elements in a list. For example what I'm trying to refine is a simple function like this

isOver :: Int -> [Int] -> Bool isOver lo xs | length xs == 0 = True | (lo < (head xs)) = isOver lo (tail xs) | otherwise = False

As can be seen isOver should be a function that checks whether all elements in the list are over some input and then returns True or False. It can of course also be implemented like this

isOver :: Int -> [Int] -> Bool isOver lo = foldl (\acc x -> acc && (lo < x)) True

How do I write a specification to check whether either implementation is safe? Or this kind of predicate cannot be written the specification and instead only assumed as true and be used as measure?

— 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/95__;!!Mih3wA!W0OVC-VwMPUgmFmz6l8YmNDzv4qPDK00mPsofeO0Ewi2yXDLTpwqCYwkE11AfU85$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OHTTFAP3BDVVFNHLJLRSRWPPANCNFSM4NGNCQMQ__;!!Mih3wA!W0OVC-VwMPUgmFmz6l8YmNDzv4qPDK00mPsofeO0Ewi2yXDLTpwqCYwkE6wWYjlx$ .

[hafizhmakmur]

So actually I'm still kinda stuck in the Sanitization exercise in Chapter 5 to the point even I skip it and back to it from time to time. As can be seen in this code my implementation is still unsafe somehow. I think I may have to make a specification too for testList to solve the problem but as you can see by this question, I also still haven't figured out how to create that. Could you refer me a resource for this "reflection"? Thank you very much. :D

[ranjitjhala]

Hi, sorry for the late reply!

For this exercise you should not use a boolean test, but incrementally "build up" the Maybe value.

For example see this blog post validateNonEmpty vs parseNonEmpty explained in this blog post https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-validate/

So, for example, create a list elts' that only contains the pairs whose index is valid, and then check if elts' includes all the elements of elts (e.g. has the same size).

Does that help?

On Wed, May 20, 2020 at 11:39 PM Hafizh Afkar Makmur < notifications@github.com> wrote:

So actually I'm still kinda stuck in the Sanitization exercise in Chapter 5 to the point even I skip it and back to it from time to time. As can be seen in this code http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1590042713_8991.hs my implementation is still unsafe somehow. I think I may have to make a specification too for testList to solve the problem but as you can see by this question, I also still haven't figured out how to create that. Could you refer me a resource for this "reflection"? Thank you very much. :D

— 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/95*issuecomment-631913608__;Iw!!Mih3wA!XBaDvuyXtMq0NwLyJtK7wm9yMhhaRXgSTdbfJ1asKGMdrCPRVyuQZ1imhtRowJfL$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OCMDMSKBBC3B5H5S3TRSTEDFANCNFSM4NGNCQMQ__;!!Mih3wA!XBaDvuyXtMq0NwLyJtK7wm9yMhhaRXgSTdbfJ1asKGMdrCPRVyuQZ1imhu9473Yl$ .

[hafizhmakmur]

It is a very exciting blog! It sounds like a foundational idea of Liquid Haskell. I wonder if you get some inspiration from this writing. I still don't succeed in creating the function. My best attempt so far is in this code but it still have the same error (apart from realizing I should change Int to Nat).

[ranjitjhala]

Ah you are almost there, basically you should use buildElts elts which has the "right" (sanitized) type, and not elts which still has the "old" (unsanitized) type.

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

that is

{-@ fromList :: x:Nat -> [(Nat, a)] -> Maybe (SparseN a x) @-} fromList :: Int -> [(Int, a)] -> Maybe (Sparse a) fromList dim elts | length bElts == length elts = Just (SP dim bElts) | otherwise = Nothing where bElts = [(i, v) | (i, v) <- elts, i < dim]

:-)

On Wed, May 27, 2020 at 12:23 AM Hafizh Afkar Makmur < notifications@github.com> wrote:

It is a very exciting blog! It sounds like a foundational idea of Liquid Haskell. I wonder if you get some inspiration from this writing. I still don't succeed in creating the function. My best attempt so far is in this code http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1590563766_9283.hs but it still have the same error (apart from realizing I should change Int to Nat).

— 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/95*issuecomment-634478741__;Iw!!Mih3wA!Qk4JjWrm1kAqyxFkZgRzdXrfC9nA2jrk5AWYU5cQZl-wqAblVDdEdKfH00LmpWJQ$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OEJQPVMMHIRT7OHET3RTS5WXANCNFSM4NGNCQMQ__;!!Mih3wA!Qk4JjWrm1kAqyxFkZgRzdXrfC9nA2jrk5AWYU5cQZl-wqAblVDdEdKfH017ozD1Y$ .

[hafizhmakmur]

Oh yeah before I have changed the Just (SP dim elts') to use the already sanitized type but then it was still not working so I changed it back. I've changed it back to your suggestion because well it makes much more sense

After some experiments and seeing your code, I've determined that the real problem is that the refiner doesn't really work around fst function. Here is the code where I change fst xs in favor of pattern recognision (see fromList and fromList') inspired by your code, and it works perfectly. I guess it's the same problem with null that I have discussed some time before. Thank you for your assistance!

(Btw I think I like my fromList' more. I think it's more coherent with the spirit of the function. Also inspired by that parse don't validate article!)