Why should 0 <= VV < acc

[kishlaya]

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

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 notifications@github.com 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 https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/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 notifications@github.com 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 https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/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 < notifications@github.com> 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 https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/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 < notifications@github.com> 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 https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/88?email_source=notifications&email_token=AAMS4OCWXPAJCAJFMF4C2XTREKRD3A5CNFSM4JMEPJR2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEMWAUFQ#issuecomment-590088726, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAMS4OBP2MGMCWM6345RDDTREKRD3ANCNFSM4JMEPJRQ .