Elemental Measures not working as described

[tferariu]

I'm following the online tutorial and trying the following code:

module Demo.Lib where

import Data.Set

{-@ measure elts @-}
elts        :: (Ord a) => [a] -> Set a
elts []     = empty
elts (x:xs) = singleton x `union` elts xs

results in an error about Set_cup and Set_empty being unbound. As far as I understand those are from the specification of Data.Set, and should just work under the hood.

Is there something I am missing here? I would expect the example code from the notebook to simply compile.

[ranjitjhala]

yikes, thanks for pointing that out -- I'll fix it!

On Tue, May 10, 2022 at 8:50 AM tferariu @.***> wrote:

I'm following the online tutorial https://urldefense.proofpoint.com/v2/url?u=https-3A__ucsd-2Dprogsys.github.io_liquidhaskell-2Dtutorial_Tutorial-5F08-5FMeasure-5FSet.html&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=7qskKLuFIkAwSpuxUSPWvAw5BCrwDFkDD9MpcAbwAe-HP51XHDCrp3K9APZ6tHvD&s=ipjI2WtbFUHOmi60o1lLmm8gmKjTjn-IIBdDG_3BYt4&e= and trying the following code:

module Demo.Lib where

import Data.Set

{-@ measure elts @-} elts :: (Ord a) => [a] -> Set a elts [] = empty elts (x:xs) = singleton x union elts xs

results in an error about Set_cup and Set_empty being unbound. As far as I understand those are from the specification https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquidhaskell_blob_master_include_Data_Set.spec&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=7qskKLuFIkAwSpuxUSPWvAw5BCrwDFkDD9MpcAbwAe-HP51XHDCrp3K9APZ6tHvD&s=XxNFMmXdhqkghciLRUN9pSv4Lx4s9x5I84e-xD4wl2I&e= of Data.Set, and should just work under the hood.

Is there something I am missing here? I would expect the example code from the notebook to simply compile.

— Reply to this email directly, view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquidhaskell_issues_1981&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=7qskKLuFIkAwSpuxUSPWvAw5BCrwDFkDD9MpcAbwAe-HP51XHDCrp3K9APZ6tHvD&s=QrQGkggLGtXofJkWZ2yvMcC5Fus-KcGdQvSrOCUUD-4&e=, or unsubscribe https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OHTD74MMP3MADV4YLLVJKAUZANCNFSM5VSBX7MA&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=7qskKLuFIkAwSpuxUSPWvAw5BCrwDFkDD9MpcAbwAe-HP51XHDCrp3K9APZ6tHvD&s=rg1lDhW2_4MGgq7kU7zTfbF5zZ69lFYagpu4sKL9r1U&e= . You are receiving this because you are subscribed to this thread.Message ID: @.***>

[tferariu]

I have had various other problems as well but this one confused me in particular. Is there any chance you can tell me what was going wrong or what I am doing wrong once you figure it out?

[ranjitjhala]

hmm the following permalink works for me -- can you confirm?

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

On Tue, May 10, 2022 at 8:57 AM tferariu @.***> wrote:

I have had various other problems as well but this one confused me in particular. Is there any chance you can tell me what was going wrong or what I am doing wrong once you figure it out?

— Reply to this email directly, view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquidhaskell_issues_1981-23issuecomment-2D1122586250&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=8z_HRaY0gN6_QcxEsvesSGXVsfKnwBuboIGU4QIIVKLnvV_qSbhLqEkz2JvtIuFL&s=x0uONZ_OtWz2Udez1cF2e_wSySL3G7x0JOA5dyttjOI&e=, or unsubscribe https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OHWP5REKNQQHXEFHOTVJKBPTANCNFSM5VSBX7MA&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=8z_HRaY0gN6_QcxEsvesSGXVsfKnwBuboIGU4QIIVKLnvV_qSbhLqEkz2JvtIuFL&s=ZLdU2Pr3GP8YbxAdg-0cJlz-cy_p4eN5Zv7J9m5qV0c&e= . You are receiving this because you commented.Message ID: @.***>

[tferariu]

That works, but I am trying to run the installation of the most recent release of the code as a plugin and it does not work that way.

[tferariu]

import Language.Haskell.Liquid.Prelude

{-@ type TRUE  = {v:Bool | v    } @-}

{-@ congruence :: (Int -> Int) -> Int -> Int -> TRUE @-}
congruence f x y = (x == y) ==> (f x == f y)

This code from the second module of the tutorial doesn't work in the online editor either.

[ranjitjhala]

ah got it, ok will take a look! (i somehow thought the issue was with the web demo!)

On Tue, May 10, 2022 at 9:15 AM tferariu @.***> wrote:

import Language.Haskell.Liquid.Prelude

{-@ type TRUE = {v:Bool | v } @-}

{-@ congruence :: (Int -> Int) -> Int -> Int -> TRUE @-} congruence f x y = (x == y) ==> (f x == f y)

This code from the second module https://urldefense.proofpoint.com/v2/url?u=https-3A__ucsd-2Dprogsys.github.io_liquidhaskell-2Dtutorial_Tutorial-5F02-5FLogic.html&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=f3A_6CNM3qwpK9DB68r4IkwauQvuaauLJe1qNZil7zQQmW6WUo-STWXWL5caDcIB&s=AuphFWlUcEfT0PaiJhO77FADy7sLbnh-hLD5ye-u33o&e= of the tutorial doesn't work in the online editor either.

— Reply to this email directly, view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquidhaskell_issues_1981-23issuecomment-2D1122605007&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=f3A_6CNM3qwpK9DB68r4IkwauQvuaauLJe1qNZil7zQQmW6WUo-STWXWL5caDcIB&s=Z8eFY_u9mJRQ1plefQ7P3sXOKV6O8rR8neYUaObfWbU&e=, or unsubscribe https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OG7JUA2LHYTHE5OTODVJKDRHANCNFSM5VSBX7MA&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=f3A_6CNM3qwpK9DB68r4IkwauQvuaauLJe1qNZil7zQQmW6WUo-STWXWL5caDcIB&s=Ky3IAmXv_XBSJXhf0OXwOldS0admWYAxcYH4dMg1hEo&e= . You are receiving this because you commented.Message ID: @.***>

[ranjitjhala]

For the congruence example, you need to

1. Specify the Haskell/GHC type of congruence and
2. Tell LH to allow functions in refinements with --reflection

So this works [but I should update the text!]

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