search

ucsd-progsys / liquidhaskell-tutorial

Tutorial for LiquidHaskell
https://ucsd-progsys.github.io/liquidhaskell-tutorial/
MIT License
74 stars 27 forks source link

Do I need to do something to enable inference? #84

Closed mpdairy closed 5 years ago

mpdairy commented 5 years ago

I'm looking at the loop example in chapter 4, and it says that LH will automatically infer the type type of loop to be:

loop :: lo:Nat -> hi:{Nat|lo <= hi} -> a -> (Btwn lo hi -> a -> a) -> a

for the function:

loop :: Int -> Int -> a -> (Int -> a -> a) -> a
loop lo hi base f =  go base lo
  where
    go acc i
      | i < hi    = go (f i acc) (i + 1)
      | otherwise = acc

But I have to manually put in the liquid type annotation or vectorSum' really won't work, and even then it actually still doesn't work because it doesn't infer the type of go.

My own loop function I made without a go works:

{-@ loop :: lo:Int -> {hi:Int | hi >= lo} -> a -> (Btwn lo hi -> a -> a) -> a @-}
loop :: Int -> Int -> a -> (Int -> a -> a) -> a
loop lo hi acc f
  | lo >= hi = acc
  | otherwise = loop (lo + 1) hi (f lo acc) f

The only two options I have on are:

{-@ LIQUID "--no-termination" @-}
{-@ LIQUID "--reflection" @-}

Also, is there a way to see the inferred types from the command line?

ranjitjhala commented 5 years ago

Hi Matt, no specific options. Can you post the gist of the source code that you are using so that I can take a look and explain what’s going on? Thanks!

On Tue, Sep 10, 2019 at 1:37 PM Matt Parker notifications@github.com wrote:

I'm looking at the loop example in chapter 4, and it says that LH will automatically infer type type of loop to be:

loop :: lo:Nat -> hi:{Nat|lo <= hi} -> a -> (Btwn lo hi -> a -> a) -> a

for the function:

loop :: Int -> Int -> a -> (Int -> a -> a) -> a loop lo hi base f = go base lo where go acc i | i < hi = go (f i acc) (i + 1) | otherwise = acc

But I have to manually put in the liquid type annotation or vectorSum' really won't work, and even then it actually still doesn't work because it doesn't infer the type of go.

My own loop function I made without a go works:

{-@ loop :: lo:Int -> {hi:Int | hi >= lo} -> a -> (Btwn lo hi -> a -> a) -> a @-} loop :: Int -> Int -> a -> (Int -> a -> a) -> a loop lo hi acc f | lo >= hi = acc | otherwise = loop (lo + 1) hi (f lo acc) f

The only two options I have on are:

{-@ LIQUID "--no-termination" @-} {-@ LIQUID "--reflection" @-}

Also, is there a way to see the inferred types from the command line?

— 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/84?email_source=notifications&email_token=AAMS4OHWSI67GESZARBJEJ3QJAAO5A5CNFSM4IVMJG2KYY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4HKRSCWA, or mute the thread https://github.com/notifications/unsubscribe-auth/AAMS4OFAPDGCJIFEIEAFX3DQJAAO5ANCNFSM4IVMJG2A .

mpdairy commented 5 years ago

Hi Ranjit, thanks for always replying so promptly! Here's the essential parts of my code. I'm still using my own vector type because I already made it previously when I couldn't get the Haskell Vector to work (which you helped me fix). Maybe my type signatures for Vector related stuff is the problem...

{-@ LIQUID "--no-termination" @-}
{-@ LIQUID "--reflection" @-}

module Blaze.Liquid.Ex5 where

import Prelude hiding (abs, length)

{-@ type Nat   = {v:Int | 0 <= v}        @-}

{-@ die :: {v:String | false} -> a  @-}
die msg = error msg

data Vector a = VNil
              | a ::: (Vector a)
              deriving (Eq, Ord, Show)

{-@ measure vlen @-}
vlen :: Vector a -> Int
vlen VNil = 0
vlen (_:::v) = 1 + vlen v

{-@ fromList :: xs:[a] -> {v:Vector a | len xs == vlen v}  @-}
fromList :: [a] -> Vector a
fromList [] = VNil
fromList (x:xs) = x ::: fromList xs

{-@ type Btwn Lo Hi = {n:Int | Lo <= n && n < Hi } @-}

{-@ (!) :: a:Vector a -> Btwn 0 (vlen a) -> a @-}
(!) :: Vector a -> Int -> a
(!) VNil _ = die "(!): index out of bounds"
(!) (x:::_) 0 = x
(!) (_:::xs) n = xs ! (n - 1)

{-@ loop :: lo:Int -> {hi:Int | hi >= lo} -> a -> (Btwn lo hi -> a -> a) -> a @-}
loop :: Int -> Int -> a -> (Int -> a -> a) -> a
loop lo hi base f =  go base lo
  where
    go acc i
      | i < hi    = go (f i acc) (i + 1)
      | otherwise = acc

{-@ vectorSum' :: {v:Vector Int | vlen v >= 0} -> Int @-}
vectorSum' :: Vector Int -> Int
vectorSum' v = loop 0 (vlen v) 0 f where
  f i acc = (v ! i) + acc

And I get the error:

 40 |       | i < hi    = go (f i acc) (i + 1)
                                ^

   Inferred type
     VV : {v : GHC.Types.Int | v == i}

   not a subtype of Required type
     VV : {VV : GHC.Types.Int | lo <= VV
                                && VV < hi}

   In Context
     hi : {hi : GHC.Types.Int | hi >= lo}

     lo : GHC.Types.Int

     i : GHC.Types.Int
ranjitjhala commented 5 years ago

Aha, so the issue is this:

  1. The --reflection actually switches off inference (reflection is used in "proof" mode where we don't use inference much...) So if you comment out that line -- and indeed for all of the tutorial (except that one-off thing in the earlier chapter) leave it off -- then your code passes.

  2. The reason LH is not inferring the signature for loop is that it is "exported" i.e. is a "public" function of the module, and for those LH doesn't do any inference.

    If you want to remove the signature for loop, then define the module as:

    module Blaze.Liquid.Ex5 () where

    or

    module Blaze.Liquid.Ex5 (vectorSum') where

    basically, don't export loop and then LH will infer the suitable type.

  3. Unfortunately we don't print out the types in the CLI (though we should have an option to!) The easiest way to see the inferred type is to open the generated HTML in a web-browser, e.g. if the source file is path/to/file.hs then open path/to/.liquid/file.hs.html and hover the mouse over the relevant identifier to see its inferred type.

LMK if this helps!

On Tue, Sep 10, 2019 at 2:01 PM Matt Parker notifications@github.com wrote:

Hi Ranjit, thanks for always replying so promptly! Here's the essential parts of my code. I'm still using my own vector type because I already made it previously when I couldn't get the Haskell Vector to work (which you helped me fix). Maybe my type signatures for Vector related stuff is the problem...

{-@ LIQUID "--no-termination" @-} {-@ LIQUID "--reflection" @-}

module Blaze.Liquid.Ex5 where

import Prelude hiding (abs, length)

{-@ type Nat = {v:Int | 0 <= v} @-}

{-@ die :: {v:String | false} -> a @-} die msg = error msg

data Vector a = VNil | a ::: (Vector a) deriving (Eq, Ord, Show)

{-@ measure vlen @-} vlen :: Vector a -> Int vlen VNil = 0 vlen (_:::v) = 1 + vlen v

{-@ fromList :: xs:[a] -> {v:Vector a | len xs == vlen v} @-} fromList :: [a] -> Vector a fromList [] = VNil fromList (x:xs) = x ::: fromList xs

{-@ type Btwn Lo Hi = {n:Int | Lo <= n && n < Hi } @-}

{-@ (!) :: a:Vector a -> Btwn 0 (vlen a) -> a @-} (!) :: Vector a -> Int -> a (!) VNil = die "(!): index out of bounds" (!) (x:::) 0 = x (!) (_:::xs) n = xs ! (n - 1)

{-@ loop :: lo:Int -> {hi:Int | hi >= lo} -> a -> (Btwn lo hi -> a -> a) -> a @-} loop :: Int -> Int -> a -> (Int -> a -> a) -> a loop lo hi base f = go base lo where go acc i | i < hi = go (f i acc) (i + 1) | otherwise = acc

{-@ vectorSum' :: {v:Vector Int | vlen v >= 0} -> Int @-} vectorSum' :: Vector Int -> Int vectorSum' v = loop 0 (vlen v) 0 f where f i acc = (v ! i) + acc

And I get the error:

40 | | i < hi = go (f i acc) (i + 1) ^

Inferred type VV : {v : GHC.Types.Int | v == i}

not a subtype of Required type VV : {VV : GHC.Types.Int | lo <= VV && VV < hi}

In Context hi : {hi : GHC.Types.Int | hi >= lo}

 lo : GHC.Types.Int

 i : GHC.Types.Int

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/84?email_source=notifications&email_token=AAMS4ODPV7M4GE4JZBRDAULQJADKZA5CNFSM4IVMJG2KYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD6MPI4A#issuecomment-530117744, or mute the thread https://github.com/notifications/unsubscribe-auth/AAMS4OE3R7NFYJV3JYLBFMDQJADKZANCNFSM4IVMJG2A .

mpdairy commented 5 years ago

Oh, thanks! That html file it generates is really neat. I didn't know about it not inferring for public functions, but maybe you say it in a previous chapter and I missed it. Thanks!

mpdairy commented 5 years ago

Also, where's the best place to ask general questions about Liquid Haskell?

ranjitjhala commented 5 years ago

The slack channel is good

https://t.co/2K0op2dKhg?amp=1

or just post issues.

On Tue, Sep 10, 2019 at 3:04 PM Matt Parker notifications@github.com wrote:

Also, where's the best place to ask general questions about Liquid Haskell?

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/84?email_source=notifications&email_token=AAMS4OEZOE72OGZ2PJ2E2O3QJAKUJA5CNFSM4IVMJG2KYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD6MUJXA#issuecomment-530138332, or mute the thread https://github.com/notifications/unsubscribe-auth/AAMS4OEQW53RUUOUCX5KXKTQJAKUJANCNFSM4IVMJG2A .