Why should 0 <= VV < acc

[kishlaya]

liquidhaskell-tutorial/src/04-poly.lhs

Line 271 in c1e1b4f

vectorSum :: Vector Int -> Int

The function vectorSum gives me a strange error:

 7 |    | i < sz = go (acc + (vec ! i)) (i + 1)
                       ^^^^^^^^^^^^^^^^^
  
   Inferred type
     VV : {v : GHC.Types.Int | v == acc + ?b}
  
   not a subtype of Required type
     VV : {VV : GHC.Types.Int | VV < acc
                                && VV >= 0}
  
   In Context
     ?b : GHC.Types.Int
      
     acc : GHC.Types.Int

As a re-check, the following code gives me the same error, when executed here

import Data.Vector
vectorSum         :: Vector Int -> Int
vectorSum vec     = go 0 0
  where
    go acc i
      | i < sz    = go (acc + (vec ! i)) (i + 1)
      | otherwise = acc
    sz            = Data.Vector.length vec

[ranjitjhala]

This is because of the termination checker which was switched on by default after the tutorial was written. My bad! For now, just run with —no-termination... Thanks for posting : Please keep this open so I fix it!

…

On Tue, Nov 12, 2019 at 6:45 AM Kishlaya ***@***.***> wrote: https://github.com/ucsd-progsys/liquidhaskell-tutorial/blob/c1e1b4ff1d6574d6cb29d9e2792c6b1c73cb05db/src/04-poly.lhs#L271 The function vectorSum gives me a strange error: 7 | | i < sz = go (acc + (vec ! i)) (i + 1) ^^^^^^^^^^^^^^^^^ Inferred type VV : {v : GHC.Types.Int | v == acc + ?b} not a subtype of Required type VV : {VV : GHC.Types.Int | VV < acc && VV >= 0} In Context ?b : GHC.Types.Int acc : GHC.Types.Int As a re-check, the following code gives me the same error, when executed here <http://goto.ucsd.edu:8090/index.html> import Data.Vector vectorSum :: Vector Int -> Int vectorSum vec = go 0 0 where go acc i | i < sz = go (acc + (vec ! i)) (i + 1) | otherwise = acc sz = Data.Vector.length vec — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#88?email_source=notifications&email_token=AAMS4OCB3Z32PSDZCFMMQUTQTK6QHA5CNFSM4JMEPJR2YY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4HYW5CDA>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAMS4OBALPLA7OKHGMGRWWTQTK6QHANCNFSM4JMEPJRQ> .

[kishlaya]

Umm, could you give me a quick insight into why does LH think that this program won't terminate?

[ranjitjhala]

Sure, see these: https://ucsd-progsys.github.io/liquidhaskell-blog/tags/termination.html briefly: your code is just fine, its Lh's default heuristics for checking termination don't apply to this program, you need an annotation to tell it what the termination "metric" is.

…

On Tue, Nov 12, 2019 at 10:16 AM Kishlaya ***@***.***> wrote: Umm, could you give me a quick insight into why does LH think that this program won't terminate? — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#88?email_source=notifications&email_token=AAMS4ODGEPUO5G6ZLITPFD3QTLW3XA5CNFSM4JMEPJR2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOED3HKRQ#issuecomment-553022790>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAMS4OD3DI3Q6CPL67ZR2VTQTLW3XANCNFSM4JMEPJRQ> .

[hafizhmakmur]

@ranjitjhala I want to note something from this problem. From chapter 2 our old problem can be solved by adding {-@ LIQUID "--reflection" @-}. Now instead it will ruin the problem for this chapter and it should not be used.

I just want to note the result of my grueling attempt to debug my failure in this very example. Thank you very much for your attention.

[ranjitjhala]

To clarify do you mean reflection should not be used in the chapter 2 or this chapter (vector bounds?)

…

On Sun, Feb 23, 2020 at 4:03 AM Hafizh Afkar Makmur < ***@***.***> wrote: @ranjitjhala <https://github.com/ranjitjhala> I want to note something from this problem. From chapter 2 our old problem can be solved by adding {-@ LIQUID "--reflection" @-}. Now instead it will ruin the problem for this chapter and it should not be used. I just want to note the result of my grueling attempt to debug my failure in this very example. Thank you very much for your attention. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#88?email_source=notifications&email_token=AAMS4OCNJG5MASLYKZMHC2DREJQXZA5CNFSM4JMEPJR2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEMVZ7UA#issuecomment-590061520>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAMS4OETPXKQHU4W74LKOXTREJQXZANCNFSM4JMEPJRQ> .

[hafizhmakmur]

Reflection should not be used in this chapter, at least in my case. vectorSum somehow will be deemed unsafe if it's added.

[ranjitjhala]

Got it, thanks!

…

On Sun, Feb 23, 2020 at 8:39 AM Hafizh Afkar Makmur < ***@***.***> wrote: Reflection should not be used in this chapter, at least in my case. vectorSum somehow will be deemed unsafe if it's added. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#88?email_source=notifications&email_token=AAMS4OCWXPAJCAJFMF4C2XTREKRD3A5CNFSM4JMEPJR2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEMWAUFQ#issuecomment-590088726>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAMS4OBP2MGMCWM6345RDDTREKRD3ANCNFSM4JMEPJRQ> .